From 2adff76c5466734c633923e768c9dcbdc6f28c86 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Tue, 23 Jun 2015 17:45:04 +0200 Subject: Add corresponding field in `VernacInductive`. Makes sure not to generate inductive schemes of assumed positive types. --- printing/ppvernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 832c08fe0e..a65bfd44d7 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -761,7 +761,7 @@ module Make (pr_assumption_token (n > 1) stre ++ spc() ++ pr_ne_params_list pr_lconstr_expr l) ) - | VernacInductive (p,f,l) -> + | VernacInductive (chk,p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ -- 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`. --- printing/printer.ml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) (limited to 'printing') diff --git a/printing/printer.ml b/printing/printer.ml index 6525428254..b57fa90797 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -729,14 +729,21 @@ let pr_assumptionset env s = try str " : " ++ pr_ltype typ with e when Errors.noncritical e -> mt () in + let pr_axiom env ax typ = + match ax with + | Constant kn -> + safe_pr_constant env kn ++ safe_pr_ltype typ + | Positive m -> + hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.") + in let fold t typ accu = let (v, a, o, tr) = accu in match t with | Variable id -> let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in (var :: v, a, o, tr) - | Axiom kn -> - let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in + | Axiom axiom -> + let ax = pr_axiom env axiom typ in (v, ax :: a, o, tr) | Opaque kn -> let opq = safe_pr_constant env kn ++ safe_pr_ltype typ in -- cgit v1.2.3 From e0547f9e9134a9fff122df900942a094c53535c3 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Fri, 26 Jun 2015 21:15:36 +0200 Subject: Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming guardedness. --- printing/ppvernac.ml | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index a65bfd44d7..93cd35472a 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -399,6 +399,15 @@ module Make | None -> mt () | Some i -> spc () ++ str "|" ++ spc () ++ int i + let pr_assume ?(positive=false) ?(guarded=false) () = + let assumed = + (if guarded then [str"Guarded"] else []) @ + (if positive then [str"Positive"] else []) + in + match assumed with + | [] -> mt () + | l -> keyword"Assume" ++ spc() ++ str"[" ++ prlist (fun x->x) l ++ str"]" ++ spc() + (**************************************) (* Pretty printer for vernac commands *) (**************************************) @@ -797,7 +806,7 @@ module Make (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) ) - | VernacFixpoint (local, recs) -> + | VernacFixpoint (chkguard,local, recs) -> let local = match local with | Some Discharge -> "Let " | Some Local -> "Local " @@ -812,11 +821,11 @@ module Make prlist (pr_decl_notation pr_constr) ntn in return ( - hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++ + hov 0 (pr_assume ~guarded:chkguard ()++str local ++ keyword "Fixpoint" ++ spc () ++ prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs) ) - | VernacCoFixpoint (local, corecs) -> + | VernacCoFixpoint (chkguard,local, corecs) -> let local = match local with | Some Discharge -> keyword "Let" ++ spc () | Some Local -> keyword "Local" ++ spc () @@ -829,7 +838,7 @@ module Make prlist (pr_decl_notation pr_constr) ntn in return ( - hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++ + hov 0 (pr_assume ~guarded:chkguard ()++local ++ keyword "CoFixpoint" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs) ) | VernacScheme l -> -- 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` --- printing/printer.ml | 2 ++ 1 file changed, 2 insertions(+) (limited to 'printing') 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 -- 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 --- printing/ppvernac.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 93cd35472a..8a8521ccc1 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -806,7 +806,7 @@ module Make (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) ) - | VernacFixpoint (chkguard,local, recs) -> + | VernacFixpoint (flags,local, recs) -> let local = match local with | Some Discharge -> "Let " | Some Local -> "Local " @@ -821,11 +821,11 @@ module Make prlist (pr_decl_notation pr_constr) ntn in return ( - hov 0 (pr_assume ~guarded:chkguard ()++str local ++ keyword "Fixpoint" ++ spc () ++ + hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++str local ++ keyword "Fixpoint" ++ spc () ++ prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs) ) - | VernacCoFixpoint (chkguard,local, corecs) -> + | VernacCoFixpoint (flags,local, corecs) -> let local = match local with | Some Discharge -> keyword "Let" ++ spc () | Some Local -> keyword "Local" ++ spc () @@ -838,7 +838,7 @@ module Make prlist (pr_decl_notation pr_constr) ntn in return ( - hov 0 (pr_assume ~guarded:chkguard ()++local ++ keyword "CoFixpoint" ++ spc() ++ + hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++local ++ keyword "CoFixpoint" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs) ) | VernacScheme l -> -- cgit v1.2.3 From dcf4d3e28813e09fc71f974b79ddf42d2e525976 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 5 Jun 2016 21:50:22 +0200 Subject: Remove the syntax changes introduced by this branch. We decided to only export the API, so that an external plugin can provide this feature without having to merge it in current Coq trunk. This postpones the attribute implementation in vernacular commands after 8.6. --- printing/ppvernac.ml | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) (limited to 'printing') diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 8a8521ccc1..832c08fe0e 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -399,15 +399,6 @@ module Make | None -> mt () | Some i -> spc () ++ str "|" ++ spc () ++ int i - let pr_assume ?(positive=false) ?(guarded=false) () = - let assumed = - (if guarded then [str"Guarded"] else []) @ - (if positive then [str"Positive"] else []) - in - match assumed with - | [] -> mt () - | l -> keyword"Assume" ++ spc() ++ str"[" ++ prlist (fun x->x) l ++ str"]" ++ spc() - (**************************************) (* Pretty printer for vernac commands *) (**************************************) @@ -770,7 +761,7 @@ module Make (pr_assumption_token (n > 1) stre ++ spc() ++ pr_ne_params_list pr_lconstr_expr l) ) - | VernacInductive (chk,p,f,l) -> + | VernacInductive (p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ @@ -806,7 +797,7 @@ module Make (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) ) - | VernacFixpoint (flags,local, recs) -> + | VernacFixpoint (local, recs) -> let local = match local with | Some Discharge -> "Let " | Some Local -> "Local " @@ -821,11 +812,11 @@ module Make prlist (pr_decl_notation pr_constr) ntn in return ( - hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++str local ++ keyword "Fixpoint" ++ spc () ++ + hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++ prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs) ) - | VernacCoFixpoint (flags,local, corecs) -> + | VernacCoFixpoint (local, corecs) -> let local = match local with | Some Discharge -> keyword "Let" ++ spc () | Some Local -> keyword "Local" ++ spc () @@ -838,7 +829,7 @@ module Make prlist (pr_decl_notation pr_constr) ntn in return ( - hov 0 (pr_assume ~guarded:flags.Declarations.check_guarded ()++local ++ keyword "CoFixpoint" ++ spc() ++ + hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++ prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs) ) | VernacScheme l -> -- cgit v1.2.3