Assume totality: dedicated type rather than bool

The rational is that

1. further typing flags may be available in the future
2. it makes it easier to trace and document the argument

11 files changed, 91 insertions, 79 deletions

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 591a7d404c..0c085df39e 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -64,6 +64,15 @@ type constant_def =
 
 type constant_universes = Univ.universe_context
 
+(** The [typing_flags] are instructions to the type-checker which
+    modify its behaviour. The typing flags used in the type-checking
+    of a constant are tracked in their {!constant_body} so that they
+    can be displayed to the user. *)
+type typing_flags = {
+  check_guarded : bool; (** If [false] then fixed points and co-fixed
+                            points are assumed to be total. *)
+}
+
 (* some contraints are in constant_constraints, some other may be in
  * the OpaueDef *)
 type constant_body = {
@@ -75,7 +84,9 @@ type constant_body = {
     const_universes : constant_universes;
     const_proj : projection_body option;
     const_inline_code : bool;
-    const_checked_guarded : bool; (** [false] is the (co)fixpoint in the constant were assumed to be well-founded. *)
+    const_typing_flags : typing_flags; (** The typing options which
+                                           were used for
+                                           type-checking. *)
 }
 
 type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 068bc498a0..98d2877373 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -133,7 +133,7 @@ let subst_const_body sub cb =
         const_polymorphic = cb.const_polymorphic;
         const_universes = cb.const_universes;
         const_inline_code = cb.const_inline_code;
-        const_checked_guarded = cb.const_checked_guarded }
+        const_typing_flags = cb.const_typing_flags }
 
 (** {7 Hash-consing of constants } *)
 
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 8c14f5e045..32583f531b 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -326,7 +326,7 @@ let type_fixpoint env lna lar vdef vdeft =
     (* ATTENTION : faudra faire le typage du contexte des Const,
     Ind et Constructsi un jour cela devient des constructions
     arbitraires et non plus des variables *)
-let rec execute ~chkguard env cstr =
+let rec execute ~flags env cstr =
   match kind_of_term cstr with
     (* Atomic terms *)
     | Sort (Prop c) ->
@@ -345,12 +345,12 @@ let rec execute ~chkguard env cstr =
       judge_of_constant env c
 	
     | Proj (p, c) ->
-        let ct = execute ~chkguard env c in
+        let ct = execute ~flags env c in
           judge_of_projection env p c ct
 
     (* Lambda calculus operators *)
     | App (f,args) ->
-        let argst = execute_array ~chkguard env args in
+        let argst = execute_array ~flags env args in
 	let ft =
 	  match kind_of_term f with
 	  | Ind ind when Environ.template_polymorphic_pind ind env ->
@@ -363,7 +363,7 @@ let rec execute ~chkguard env cstr =
 	      judge_of_constant_knowing_parameters env cst args
 	  | _ ->
 	    (* Full or no sort-polymorphism *)
-	    execute ~chkguard env f
+            execute ~flags env f
 	in
 
 	  judge_of_apply env f ft args argst
@@ -371,25 +371,25 @@ let rec execute ~chkguard env cstr =
     | Lambda (name,c1,c2) ->
       let _ = execute_is_type env c1 in
       let env1 = push_rel (name,None,c1) env in
-      let c2t = execute ~chkguard env1 c2 in
+      let c2t = execute ~flags env1 c2 in
         judge_of_abstraction env name c1 c2t
 
     | Prod (name,c1,c2) ->
-      let vars = execute_is_type ~chkguard env c1 in
+      let vars = execute_is_type ~flags env c1 in
       let env1 = push_rel (name,None,c1) env in
-      let vars' = execute_is_type ~chkguard env1 c2 in
+      let vars' = execute_is_type ~flags env1 c2 in
 	judge_of_product env name vars vars'
 
     | LetIn (name,c1,c2,c3) ->
-      let c1t = execute ~chkguard env c1 in
+      let c1t = execute ~flags env c1 in
       let _c2s = execute_is_type env c2 in
       let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in
       let env1 = push_rel (name,Some c1,c2) env in
-      let c3t = execute ~chkguard env1 c3 in
+      let c3t = execute ~flags env1 c3 in
 	subst1 c1 c3t
 
     | Cast (c,k,t) ->
-      let ct = execute ~chkguard env c in
+      let ct = execute ~flags env c in
       let _ts = execute_type env t in
       let _ = judge_of_cast env c ct k t in
 	t
@@ -402,20 +402,20 @@ let rec execute ~chkguard env cstr =
       judge_of_constructor env c
 
     | Case (ci,p,c,lf) ->
-        let ct = execute ~chkguard env c in
-        let pt = execute ~chkguard env p in
-        let lft = execute_array ~chkguard env lf in
+        let ct = execute ~flags env c in
+        let pt = execute ~flags env p in
+        let lft = execute_array ~flags env lf in
           judge_of_case env ci p pt c ct lf lft
 
     | Fix ((vn,i as vni),recdef) ->
-      let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in
+      let (fix_ty,recdef') = execute_recdef ~flags env recdef i in
       let fix = (vni,recdef') in
-        check_fix env ~chk:chkguard fix; fix_ty
+        check_fix env ~flags fix; fix_ty
 	  
     | CoFix (i,recdef) ->
-      let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in
+      let (fix_ty,recdef') = execute_recdef ~flags env recdef i in
       let cofix = (i,recdef') in
-        check_cofix env ~chk:chkguard cofix; fix_ty
+        check_cofix env ~flags cofix; fix_ty
 	  
     (* Partial proofs: unsupported by the kernel *)
     | Meta _ ->
@@ -424,41 +424,41 @@ let rec execute ~chkguard env cstr =
     | Evar _ ->
 	anomaly (Pp.str "the kernel does not support existential variables")
 
-and execute_is_type ~chkguard env constr =
-  let t = execute ~chkguard env constr in
+and execute_is_type ~flags env constr =
+  let t = execute ~flags env constr in
     check_type env constr t
 
-and execute_type ~chkguard env constr =
-  let t = execute ~chkguard env constr in
+and execute_type ~flags env constr =
+  let t = execute ~flags env constr in
     type_judgment env constr t
 
-and execute_recdef ~chkguard env (names,lar,vdef) i =
-  let lart = execute_array ~chkguard env lar in
+and execute_recdef ~flags env (names,lar,vdef) i =
+  let lart = execute_array ~flags env lar in
   let lara = Array.map2 (assumption_of_judgment env) lar lart in
   let env1 = push_rec_types (names,lara,vdef) env in
-  let vdeft = execute_array ~chkguard env1 vdef in
+  let vdeft = execute_array ~flags env1 vdef in
   let () = type_fixpoint env1 names lara vdef vdeft in
     (lara.(i),(names,lara,vdef))
 
-and execute_array ~chkguard env = Array.map (execute ~chkguard env)
+and execute_array ~flags env = Array.map (execute ~flags env)
 
 (* Derived functions *)
-let infer ~chkguard env constr =
-  let t = execute ~chkguard env constr in
+let infer ~flags env constr =
+  let t = execute ~flags env constr in
     make_judge constr t
 
 let infer = 
   if Flags.profile then
     let infer_key = Profile.declare_profile "Fast_infer" in
-      Profile.profile3 infer_key (fun a b c -> infer ~chkguard:a b c)
-  else (fun a b c -> infer ~chkguard:a b c)
+      Profile.profile3 infer_key (fun a b c -> infer ~flags:a b c)
+  else (fun a b c -> infer ~flags:a b c)
 
 (* Restores the labels of [infer] lost to profiling. *)
-let infer ~chkguard env t = infer chkguard env t
+let infer ~flags env t = infer flags env t
 
-let infer_type ~chkguard env constr =
-  execute_type ~chkguard env constr
+let infer_type ~flags env constr =
+  execute_type ~flags env constr
 
-let infer_v ~chkguard env cv =
-  let jv = execute_array ~chkguard env cv in
+let infer_v ~flags env cv =
+  let jv = execute_array ~flags env cv in
     make_judgev cv jv
diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli
index 98dbefad13..1c0146baea 100644
--- a/kernel/fast_typeops.mli
+++ b/kernel/fast_typeops.mli
@@ -8,6 +8,7 @@
 
 open Term
 open Environ
+open Declarations
 
 (** {6 Typing functions (not yet tagged as safe) }
     
@@ -18,6 +19,6 @@ open Environ
  *)
 
 
-val infer      : chkguard:bool -> env -> constr       -> unsafe_judgment
-val infer_v    : chkguard:bool -> env -> constr array -> unsafe_judgment array
-val infer_type : chkguard:bool -> env -> types        -> unsafe_type_judgment
+val infer      : flags:typing_flags -> env -> constr       -> unsafe_judgment
+val infer_v    : flags:typing_flags -> env -> constr array -> unsafe_judgment array
+val infer_type : flags:typing_flags -> env -> types        -> unsafe_type_judgment
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 532287c304..fdca5ce26b 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1065,8 +1065,8 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
   (Array.map fst rv, Array.map snd rv)
 
 
-let check_fix env ~chk ((nvect,_),(names,_,bodies as recdef) as fix) =
-  if chk then
+let check_fix env ~flags ((nvect,_),(names,_,bodies as recdef) as fix) =
+  if flags.check_guarded then
     let (minds, rdef) = inductive_of_mutfix env fix in
     let get_tree (kn,i) =
       let mib = Environ.lookup_mind kn env in
@@ -1193,8 +1193,8 @@ let check_one_cofix env nbfix def deftype =
 (* The  function which checks that the whole block of definitions
    satisfies the guarded condition *)
 
-let check_cofix env ~chk (bodynum,(names,types,bodies as recdef)) =
-  if chk then
+let check_cofix env ~flags (bodynum,(names,types,bodies as recdef)) =
+  if flags.check_guarded then
     let nbfix = Array.length bodies in
     for i = 0 to nbfix-1 do
       let fixenv = push_rec_types recdef env in
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 36f32b30c6..54036d86aa 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -98,8 +98,8 @@ val check_case_info : env -> pinductive -> case_info -> unit
 
 (** When [chk] is false, the guard condition is not actually
     checked. *)
-val check_fix : env -> chk:bool -> fixpoint -> unit
-val check_cofix : env -> chk:bool -> cofixpoint -> unit
+val check_fix : env -> flags:typing_flags -> fixpoint -> unit
+val check_cofix : env -> flags:typing_flags -> cofixpoint -> unit
 
 (** {6 Support for sort-polymorphic inductive types } *)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 18d8978174..2cea50d9ec 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -332,8 +332,8 @@ let safe_push_named (id,_,_ as d) env =
   Environ.push_named d env
 
 
-let push_named_def ~chkguard (id,de) senv =
-  let c,typ,univs = Term_typing.translate_local_def ~chkguard senv.env id de in
+let push_named_def ~flags (id,de) senv =
+  let c,typ,univs = Term_typing.translate_local_def ~flags senv.env id de in
   let senv' = push_context univs senv in
   let c, senv' = match c with
     | Def c -> Mod_subst.force_constr c, senv'
@@ -346,9 +346,9 @@ let push_named_def ~chkguard (id,de) senv =
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
     {senv' with env=env''}
 
-let push_named_assum ~chkguard ((id,t),ctx) senv =
+let push_named_assum ~flags ((id,t),ctx) senv =
   let senv' = push_context_set ctx senv in
-  let t = Term_typing.translate_local_assum ~chkguard senv'.env t in
+  let t = Term_typing.translate_local_assum ~flags senv'.env t in
   let env'' = safe_push_named (id,None,t) senv'.env in
     {senv' with env=env''}
 
@@ -439,14 +439,14 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
 
 (** Insertion of constants and parameters in environment *)
 type global_declaration =
-  | ConstantEntry of Entries.constant_entry * bool (* check guard *)
+  | ConstantEntry of Entries.constant_entry * Declarations.typing_flags
   | GlobalRecipe of Cooking.recipe
 
 let add_constant dir l decl senv =
   let kn = make_con senv.modpath dir l in
   let cb = match decl with
-    | ConstantEntry (ce,chkguard) ->
-        Term_typing.translate_constant ~chkguard senv.env kn ce
+    | ConstantEntry (ce,flags) ->
+        Term_typing.translate_constant ~flags senv.env kn ce
     | GlobalRecipe r ->
       let cb = Term_typing.translate_recipe senv.env kn r in
       if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 80b9bb495a..c5e43e42ac 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -57,16 +57,16 @@ val is_joined_environment : safe_environment -> bool
 (** Insertion of local declarations (Local or Variables) *)
 
 val push_named_assum :
-  chkguard:bool ->
+  flags:Declarations.typing_flags ->
   (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0
 val push_named_def :
-  chkguard:bool ->
+  flags:Declarations.typing_flags ->
   Id.t * Entries.definition_entry -> safe_transformer0
 
 (** Insertion of global axioms or definitions *)
 
 type global_declaration =
-  | ConstantEntry of Entries.constant_entry * bool (* chkguard *)
+  | ConstantEntry of Entries.constant_entry * Declarations.typing_flags
   | GlobalRecipe of Cooking.recipe
 
 val add_constant :
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 8a105ac971..64597469a8 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -23,18 +23,18 @@ open Entries
 open Typeops
 open Fast_typeops
 
-let constrain_type ~chkguard env j poly subst = function
+let constrain_type ~flags env j poly subst = function
   | `None -> 
     if not poly then (* Old-style polymorphism *)
       make_polymorphic_if_constant_for_ind env j
     else RegularArity (Vars.subst_univs_level_constr subst j.uj_type)
   | `Some t ->
-      let tj = infer_type ~chkguard env t in
+      let tj = infer_type ~flags env t in
       let _ = judge_of_cast env j DEFAULTcast tj in
 	assert (eq_constr t tj.utj_val);
 	RegularArity (Vars.subst_univs_level_constr subst t)
   | `SomeWJ (t, tj) ->
-      let tj = infer_type ~chkguard env t in
+      let tj = infer_type ~flags env t in
       let _ = judge_of_cast env j DEFAULTcast tj in
 	assert (eq_constr t tj.utj_val);
 	RegularArity (Vars.subst_univs_level_constr subst t)
@@ -101,11 +101,11 @@ let hcons_j j =
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
 
-let infer_declaration ~chkguard env kn dcl =
+let infer_declaration ~flags env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
       let env = push_context uctx env in
-      let j = infer ~chkguard env t in
+      let j = infer ~flags env t in
       let abstract = poly && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract uctx in
       let c = Typeops.assumption_of_judgment env j in
@@ -122,7 +122,7 @@ let infer_declaration ~chkguard env kn dcl =
         Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) ->
           let body = handle_side_effects env body side_eff in
 	  let env' = push_context_set ctx env in
-          let j = infer ~chkguard env' body in
+          let j = infer ~flags env' body in
           let j = hcons_j j in
 	  let subst = Univ.LMap.empty in
           let _typ = constrain_type env' j c.const_entry_polymorphic subst
@@ -143,8 +143,8 @@ let infer_declaration ~chkguard env kn dcl =
       let body = handle_side_effects env body side_eff in
       let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in
-      let j = infer ~chkguard env body in
-      let typ = constrain_type ~chkguard env j c.const_entry_polymorphic usubst (map_option_typ typ) in
+      let j = infer ~flags env body in
+      let typ = constrain_type ~flags env j c.const_entry_polymorphic usubst (map_option_typ typ) in
       let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
       let def = 
 	if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty)))
@@ -186,7 +186,7 @@ let record_aux env s1 s2 =
 let suggest_proof_using = ref (fun _ _ _ _ _ -> ())
 let set_suggest_proof_using f = suggest_proof_using := f
 
-let build_constant_declaration ~chkguard kn env (def,typ,proj,poly,univs,inline_code,ctx) =
+let build_constant_declaration ~flags kn env (def,typ,proj,poly,univs,inline_code,ctx) =
   let check declared inferred =
     let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
@@ -262,25 +262,25 @@ let build_constant_declaration ~chkguard kn env (def,typ,proj,poly,univs,inline_
     const_polymorphic = poly;
     const_universes = univs;
     const_inline_code = inline_code;
-    const_checked_guarded = chkguard }
+    const_typing_flags = flags }
 
 
 (*s Global and local constant declaration. *)
 
-let translate_constant ~chkguard env kn ce =
-  build_constant_declaration ~chkguard kn env (infer_declaration ~chkguard env (Some kn) ce)
+let translate_constant ~flags env kn ce =
+  build_constant_declaration ~flags kn env (infer_declaration ~flags env (Some kn) ce)
 
-let translate_local_assum ~chkguard env t =
-  let j = infer ~chkguard env t in
+let translate_local_assum ~flags env t =
+  let j = infer ~flags env t in
   let t = Typeops.assumption_of_judgment env j in
     t
 
 let translate_recipe env kn r =
-  build_constant_declaration ~chkguard:true kn env (Cooking.cook_constant env r)
+  build_constant_declaration ~flags:{check_guarded=true} kn env (Cooking.cook_constant env r)
 
-let translate_local_def ~chkguard env id centry =
+let translate_local_def ~flags env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =
-    infer_declaration ~chkguard env None (DefinitionEntry centry) in
+    infer_declaration ~flags env None (DefinitionEntry centry) in
   let typ = type_of_constant_type env typ in
   def, typ, univs
 
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index ba4d96a5f0..f167603a79 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,10 +12,10 @@ open Environ
 open Declarations
 open Entries
 
-val translate_local_def : chkguard:bool -> env -> Id.t -> definition_entry ->
+val translate_local_def : flags:typing_flags -> env -> Id.t -> definition_entry ->
   constant_def * types * constant_universes
 
-val translate_local_assum : chkguard:bool -> env -> types -> types
+val translate_local_assum : flags:typing_flags -> env -> types -> types
 
 val mk_pure_proof : constr -> proof_output
 
@@ -28,7 +28,7 @@ val handle_entry_side_effects : env -> definition_entry -> definition_entry
     {!Entries.const_entry_body} field. It is meant to get a term out of a not
     yet type checked proof. *)
 
-val translate_constant : chkguard:bool -> env -> constant -> constant_entry -> constant_body
+val translate_constant : flags:typing_flags -> env -> constant -> constant_entry -> constant_body
 
 val translate_mind :
   env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
@@ -37,11 +37,11 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : chkguard:bool -> env -> constant option -> 
+val infer_declaration : flags:typing_flags -> env -> constant option ->
   constant_entry -> Cooking.result
 
 val build_constant_declaration :
-  chkguard:bool -> constant -> env -> Cooking.result -> constant_body
+  flags:typing_flags -> constant -> env -> Cooking.result -> constant_body
 
 val set_suggest_proof_using :
   (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 9e9f18aaa9..1c3117725c 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -494,13 +494,13 @@ let rec execute env cstr =
     | Fix ((vn,i as vni),recdef) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
       let fix = (vni,recdef') in
-        check_fix ~chk:true env fix;
+        check_fix ~flags:{check_guarded=true} env fix;
 	make_judge (mkFix fix) fix_ty
 	  
     | CoFix (i,recdef) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
       let cofix = (i,recdef') in
-        check_cofix ~chk:true env cofix;
+        check_cofix ~flags:{check_guarded=true} env cofix;
 	(make_judge (mkCoFix cofix) fix_ty)
 	  
     (* Partial proofs: unsupported by the kernel *)