diff options
| author | Arnaud Spiwack | 2015-09-25 15:11:01 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-09-25 15:11:01 +0200 |
| commit | 8886dfd8fbb53d8305f2aa72afab8377b3fa75b7 (patch) | |
| tree | 298827ee49b092dd23e7b584904c6d2e74666ef9 | |
| parent | caf8402e4af75d85223e10cba68a6a145e050dab (diff) | |
Show assumptions of well-foundedness in `Print Assumptions`
| -rw-r--r-- | library/assumptions.ml | 12 | ||||
| -rw-r--r-- | library/assumptions.mli | 1 | ||||
| -rw-r--r-- | printing/printer.ml | 2 |
3 files changed, 13 insertions, 2 deletions
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. *) diff --git a/printing/printer.ml b/printing/printer.ml index b57fa90797..8609b19c9a 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -735,6 +735,8 @@ let pr_assumptionset env s = safe_pr_constant env kn ++ safe_pr_ltype typ | Positive m -> hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.") + | Guarded kn -> + hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.") in let fold t typ accu = let (v, a, o, tr) = accu in |