From 9a1e80524e1650311b019fedbd7e774242d80ea4 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 23 Jun 2015 09:24:43 +0200
Subject: Add a corresponding field in `mutual_inductive_entry` (part 1).

The field in `mutual_inductive_entry` requires that a mutually inductive definition be checked or not, whereas the field in `mutual_inductive_body` asserts that it has or has not been.
---
 library/declare.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index c3181e4c75..02e6daddeb 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -366,7 +366,8 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
   mind_entry_polymorphic = false;
   mind_entry_universes = Univ.UContext.empty;
-  mind_entry_private = None })
+  mind_entry_private = None;
+  mind_entry_check_positivity = true; })
 
 type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry
 
-- 
cgit v1.2.3


From 476189527703aaf9caf5612e8395ce3b8ddb088f Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Wed, 24 Jun 2015 16:10:29 +0200
Subject: Make inductives that were assumed positive appear in `Print
 Assumptions`.

They appear as axioms of the form `Foo is positive`.
---
 library/assumptions.ml  | 26 ++++++++++++++++++++++----
 library/assumptions.mli |  7 +++++--
 2 files changed, 27 insertions(+), 6 deletions(-)

(limited to 'library')

diff --git a/library/assumptions.ml b/library/assumptions.ml
index 62645b2365..b2363bce61 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -23,9 +23,12 @@ open Declarations
 open Mod_subst
 open Globnames
 
+type axiom =
+  | Constant of constant (* An axiom or a constant. *)
+  | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
-  | Axiom of constant      (* An axiom or a constant. *)
+  | Axiom of axiom      (* An assumed fact. *)
   | Opaque of constant     (* An opaque constant. *)
   | Transparent of constant
 
@@ -33,10 +36,20 @@ type context_object =
 module OrderedContextObject =
 struct
   type t = context_object
+
+  let compare_axiom x y =
+    match x,y with
+    | Constant k1 , Constant k2 ->
+        con_ord k1 k2
+    | Positive m1 , Positive m2 ->
+        MutInd.CanOrd.compare m1 m2
+    | Positive _ , Constant _ -> 1
+    | _ -> -1
+
   let compare x y =
       match x , y with
       | Variable i1 , Variable i2 -> Id.compare i1 i2
-      | Axiom k1 , Axiom k2 -> con_ord k1 k2
+      | Axiom a1 , Axiom a2 -> compare_axiom a1 a2
       | Opaque k1 , Opaque k2 -> con_ord k1 k2
       | Transparent k1 , Transparent k2 -> con_ord k1 k2
       | Axiom _ , Variable _ -> 1
@@ -211,7 +224,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st t =
     let cb = lookup_constant kn in
     if not (Declareops.constant_has_body cb) then
       let t = type_of_constant cb in
-      ContextObjectMap.add (Axiom kn) t accu
+      ContextObjectMap.add (Axiom (Constant kn)) t accu
     else if add_opaque && (Declareops.is_opaque cb || not (Cpred.mem kn knst)) then
       let t = type_of_constant cb in
       ContextObjectMap.add (Opaque kn) t accu
@@ -220,6 +233,11 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st t =
       ContextObjectMap.add (Transparent kn) t accu
     else
       accu
-  | IndRef _ | ConstructRef _ -> accu
+  | IndRef (m,_) | ConstructRef ((m,_),_) ->
+      let mind = Global.lookup_mind m in
+      if mind.mind_checked_positive then
+        accu
+      else
+        ContextObjectMap.add (Axiom (Positive m)) Constr.mkProp accu
   in
   Refmap.fold fold graph ContextObjectMap.empty
diff --git a/library/assumptions.mli b/library/assumptions.mli
index bb36a97259..72ed6acf0d 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -13,9 +13,12 @@ open Globnames
 
 (** A few declarations for the "Print Assumption" command
     @author spiwack *)
+type axiom =
+  | Constant of constant (** An axiom or a constant. *)
+  | Positive of MutInd.t (** A mutually inductive definition which has been assumed positive. *)
 type context_object =
-  | Variable of Id.t  (** A section variable or a Let definition *)
-  | Axiom of constant       (** An axiom or a constant. *)
+  | Variable of Id.t  (** A section variable or a Let definition. *)
+  | Axiom of axiom       (** An assumed fact. *)
   | Opaque of constant      (** An opaque constant. *)
   | Transparent of constant (** A transparent constant *)
 
-- 
cgit v1.2.3


From e8bad8abc7be351a34fdf9770409bbab14bcd6a9 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 24 Jul 2015 08:46:09 +0200
Subject: Propagate `Guarded` flag from syntax to kernel.

The path is quite a bit of a maze, this commit is not as simple as it ought to be. Something more robust than a boolean should be used here.
---
 library/declare.ml  | 18 +++++++++---------
 library/declare.mli |  2 ++
 library/global.ml   |  4 ++--
 library/global.mli  |  6 ++++--
 4 files changed, 17 insertions(+), 13 deletions(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 02e6daddeb..4be13109af 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -50,11 +50,11 @@ let cache_variable ((sp,_),o) =
 
   let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
     | SectionLocalAssum ((ty,ctx),poly,impl) ->
-      let () = Global.push_named_assum ((id,ty),ctx) in
+      let () = Global.push_named_assum ~chkguard:true ((id,ty),ctx) in
       let impl = if impl then Implicit else Explicit in
 	impl, true, poly, ctx
     | SectionLocalDef (de) ->
-      let () = Global.push_named_def (id,de) in
+      let () = Global.push_named_def ~chkguard:true (id,de) in
         Explicit, de.const_entry_opaque, de.const_entry_polymorphic, 
 	(Univ.ContextSet.of_context de.const_entry_universes) in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
@@ -156,7 +156,7 @@ let discharge_constant ((sp, kn), obj) =
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = 
-  ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None))
+  ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), true)
 
 let dummy_constant cst = {
   cst_decl = dummy_constant_entry;
@@ -232,7 +232,7 @@ let declare_sideff env fix_exn se =
         const_entry_feedback = None;
 	const_entry_polymorphic = cb.const_polymorphic;
 	const_entry_universes = univs;
-    });
+      }, true);
     cst_hyps = [] ;
     cst_kind =  Decl_kinds.IsDefinition Decl_kinds.Definition;
     cst_locl = true;
@@ -253,7 +253,7 @@ let declare_sideff env fix_exn se =
                if Constant.equal c c' then Some (x,kn) else None) inds_consts)
            knl))
 
-let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
+let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
   let cd = (* We deal with side effects *)
     match cd with
     | Entries.DefinitionEntry de ->
@@ -275,7 +275,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff
     | _ -> cd
   in
   let cst = {
-    cst_decl = ConstantEntry cd;
+    cst_decl = ConstantEntry (cd,chkguard);
     cst_hyps = [] ;
     cst_kind = kind;
     cst_locl = local;
@@ -283,13 +283,13 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id ?(export_seff
   let kn = declare_constant_common id cst in
   kn
 
-let declare_definition ?(internal=UserVerbose) 
+let declare_definition ?chkguard ?(internal=UserVerbose) 
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
   ?(poly=false) id ?types (body,ctx) =
   let cb = 
     definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
   in
-    declare_constant ~internal ~local id
+    declare_constant ?chkguard ~internal ~local id
       (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
 
 (** Declaration of inductive blocks *)
@@ -387,7 +387,7 @@ let declare_projections mind =
       Array.iteri (fun i kn -> 
 	let id = Label.to_id (Constant.label kn) in
 	let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
-	let kn' = declare_constant id (ProjectionEntry entry,
+	let kn' = declare_constant ~chkguard:true id (ProjectionEntry entry,
 				       IsDefinition StructureComponent) 
 	in
 	  assert(eq_constant kn kn')) kns; true
diff --git a/library/declare.mli b/library/declare.mli
index d8a00db0cf..94cebe3bdc 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -53,9 +53,11 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types ->
   constr -> definition_entry
 
 val declare_constant :
+  ?chkguard:bool -> (** default [true] (check guardedness) *)
  ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
 
 val declare_definition : 
+  ?chkguard:bool -> (** default [true] (check guardedness) *)
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
   constr Univ.in_universe_context_set -> constant
diff --git a/library/global.ml b/library/global.ml
index 49fa2ef28f..27f7f52660 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -77,8 +77,8 @@ let globalize_with_summary fs f =
 
 let i2l = Label.of_id
 
-let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
-let push_named_def d = globalize0 (Safe_typing.push_named_def d)
+let push_named_assum ~chkguard a = globalize0 (Safe_typing.push_named_assum ~chkguard a)
+let push_named_def ~chkguard d = globalize0 (Safe_typing.push_named_def ~chkguard d)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set c = globalize0 (Safe_typing.push_context_set c)
 let push_context c = globalize0 (Safe_typing.push_context c)
diff --git a/library/global.mli b/library/global.mli
index 248e1f86dd..388fee5278 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -31,8 +31,10 @@ val set_type_in_type : unit -> unit
 
 (** Variables, Local definitions, constants, inductive types *)
 
-val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit
-val push_named_def   : (Id.t * Entries.definition_entry) -> unit
+val push_named_assum : 
+  chkguard:bool -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit
+val push_named_def   :
+  chkguard:bool -> (Id.t * Entries.definition_entry) -> unit
 
 val add_constant :
   DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant
-- 
cgit v1.2.3


From 8886dfd8fbb53d8305f2aa72afab8377b3fa75b7 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 25 Sep 2015 15:11:01 +0200
Subject: Show assumptions of well-foundedness in `Print Assumptions`

---
 library/assumptions.ml  | 12 ++++++++++--
 library/assumptions.mli |  1 +
 2 files changed, 11 insertions(+), 2 deletions(-)

(limited to 'library')

diff --git a/library/assumptions.ml b/library/assumptions.ml
index b2363bce61..4635278202 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -26,6 +26,7 @@ open Globnames
 type axiom =
   | Constant of constant (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
+  | Guarded of constant (* a constant whose (co)fixpoints have been assumed to be guarded *)
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
   | Axiom of axiom      (* An assumed fact. *)
@@ -43,7 +44,10 @@ struct
         con_ord k1 k2
     | Positive m1 , Positive m2 ->
         MutInd.CanOrd.compare m1 m2
-    | Positive _ , Constant _ -> 1
+    | Guarded k1 , Guarded k2 ->
+        con_ord k1 k2
+    | _ , Constant _ -> 1
+    | _ , Positive _ -> 1
     | _ -> -1
 
   let compare x y =
@@ -221,7 +225,11 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st t =
     if Option.is_empty body then ContextObjectMap.add (Variable id) t accu
     else accu
   | ConstRef kn ->
-    let cb = lookup_constant kn in
+      let cb = lookup_constant kn in
+      let accu =
+        if cb.const_checked_guarded then accu
+        else ContextObjectMap.add (Axiom (Guarded kn)) Constr.mkProp accu
+      in
     if not (Declareops.constant_has_body cb) then
       let t = type_of_constant cb in
       ContextObjectMap.add (Axiom (Constant kn)) t accu
diff --git a/library/assumptions.mli b/library/assumptions.mli
index 72ed6acf0d..499e2b42e4 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -16,6 +16,7 @@ open Globnames
 type axiom =
   | Constant of constant (** An axiom or a constant. *)
   | Positive of MutInd.t (** A mutually inductive definition which has been assumed positive. *)
+  | Guarded of constant (** A constant whose (co)fixpoints have been assumed to be guarded *)
 type context_object =
   | Variable of Id.t  (** A section variable or a Let definition. *)
   | Axiom of axiom       (** An assumed fact. *)
-- 
cgit v1.2.3


From d4f3a1a807d474050a4e91e16ff7813f1db7f537 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 7 Jun 2016 09:52:43 +0200
Subject: 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
---
 library/assumptions.ml |  2 +-
 library/declare.ml     | 18 +++++++++---------
 library/declare.mli    |  4 ++--
 library/global.ml      |  4 ++--
 library/global.mli     |  4 ++--
 5 files changed, 16 insertions(+), 16 deletions(-)

(limited to 'library')

diff --git a/library/assumptions.ml b/library/assumptions.ml
index 4635278202..f374f6dbe0 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -227,7 +227,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st t =
   | ConstRef kn ->
       let cb = lookup_constant kn in
       let accu =
-        if cb.const_checked_guarded then accu
+        if cb.const_typing_flags.check_guarded then accu
         else ContextObjectMap.add (Axiom (Guarded kn)) Constr.mkProp accu
       in
     if not (Declareops.constant_has_body cb) then
diff --git a/library/declare.ml b/library/declare.ml
index 4be13109af..c49284bbcd 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -50,11 +50,11 @@ let cache_variable ((sp,_),o) =
 
   let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
     | SectionLocalAssum ((ty,ctx),poly,impl) ->
-      let () = Global.push_named_assum ~chkguard:true ((id,ty),ctx) in
+      let () = Global.push_named_assum ~flags:{check_guarded=true} ((id,ty),ctx) in
       let impl = if impl then Implicit else Explicit in
 	impl, true, poly, ctx
     | SectionLocalDef (de) ->
-      let () = Global.push_named_def ~chkguard:true (id,de) in
+      let () = Global.push_named_def ~flags:{check_guarded=true} (id,de) in
         Explicit, de.const_entry_opaque, de.const_entry_polymorphic, 
 	(Univ.ContextSet.of_context de.const_entry_universes) in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
@@ -156,7 +156,7 @@ let discharge_constant ((sp, kn), obj) =
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = 
-  ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), true)
+  ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), {check_guarded=true})
 
 let dummy_constant cst = {
   cst_decl = dummy_constant_entry;
@@ -232,7 +232,7 @@ let declare_sideff env fix_exn se =
         const_entry_feedback = None;
 	const_entry_polymorphic = cb.const_polymorphic;
 	const_entry_universes = univs;
-      }, true);
+      }, {check_guarded=true});
     cst_hyps = [] ;
     cst_kind =  Decl_kinds.IsDefinition Decl_kinds.Definition;
     cst_locl = true;
@@ -253,7 +253,7 @@ let declare_sideff env fix_exn se =
                if Constant.equal c c' then Some (x,kn) else None) inds_consts)
            knl))
 
-let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
+let declare_constant ?(flags={check_guarded=true}) ?(internal = UserVerbose) ?(local = false) id ?(export_seff=false) (cd, kind) =
   let cd = (* We deal with side effects *)
     match cd with
     | Entries.DefinitionEntry de ->
@@ -275,7 +275,7 @@ let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false)
     | _ -> cd
   in
   let cst = {
-    cst_decl = ConstantEntry (cd,chkguard);
+    cst_decl = ConstantEntry (cd,flags);
     cst_hyps = [] ;
     cst_kind = kind;
     cst_locl = local;
@@ -283,13 +283,13 @@ let declare_constant ?(chkguard=true) ?(internal = UserVerbose) ?(local = false)
   let kn = declare_constant_common id cst in
   kn
 
-let declare_definition ?chkguard ?(internal=UserVerbose) 
+let declare_definition ?flags ?(internal=UserVerbose)
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
   ?(poly=false) id ?types (body,ctx) =
   let cb = 
     definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
   in
-    declare_constant ?chkguard ~internal ~local id
+    declare_constant ?flags ~internal ~local id
       (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
 
 (** Declaration of inductive blocks *)
@@ -387,7 +387,7 @@ let declare_projections mind =
       Array.iteri (fun i kn -> 
 	let id = Label.to_id (Constant.label kn) in
 	let entry = {proj_entry_ind = mind; proj_entry_arg = i} in
-	let kn' = declare_constant ~chkguard:true id (ProjectionEntry entry,
+        let kn' = declare_constant ~flags:{check_guarded=true} id (ProjectionEntry entry,
 				       IsDefinition StructureComponent) 
 	in
 	  assert(eq_constant kn kn')) kns; true
diff --git a/library/declare.mli b/library/declare.mli
index 94cebe3bdc..cda8855d27 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -53,11 +53,11 @@ val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types ->
   constr -> definition_entry
 
 val declare_constant :
-  ?chkguard:bool -> (** default [true] (check guardedness) *)
+  ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *)
  ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant
 
 val declare_definition : 
-  ?chkguard:bool -> (** default [true] (check guardedness) *)
+  ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *)
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
   constr Univ.in_universe_context_set -> constant
diff --git a/library/global.ml b/library/global.ml
index 27f7f52660..ab326e37d6 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -77,8 +77,8 @@ let globalize_with_summary fs f =
 
 let i2l = Label.of_id
 
-let push_named_assum ~chkguard a = globalize0 (Safe_typing.push_named_assum ~chkguard a)
-let push_named_def ~chkguard d = globalize0 (Safe_typing.push_named_def ~chkguard d)
+let push_named_assum ~flags a = globalize0 (Safe_typing.push_named_assum ~flags a)
+let push_named_def ~flags d = globalize0 (Safe_typing.push_named_def ~flags d)
 let add_constraints c = globalize0 (Safe_typing.add_constraints c)
 let push_context_set c = globalize0 (Safe_typing.push_context_set c)
 let push_context c = globalize0 (Safe_typing.push_context c)
diff --git a/library/global.mli b/library/global.mli
index 388fee5278..f7306fe570 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -32,9 +32,9 @@ val set_type_in_type : unit -> unit
 (** Variables, Local definitions, constants, inductive types *)
 
 val push_named_assum : 
-  chkguard:bool -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit
+  flags:Declarations.typing_flags -> (Id.t * Constr.types) Univ.in_universe_context_set -> unit
 val push_named_def   :
-  chkguard:bool -> (Id.t * Entries.definition_entry) -> unit
+  flags:Declarations.typing_flags -> (Id.t * Entries.definition_entry) -> unit
 
 val add_constant :
   DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant
-- 
cgit v1.2.3