Add syntax entry to assume strict positivity of an inductive type.

The syntax is `Assume [Positive]` Inductive/CoInductive/Record…`. The square brackets are used to delimit what is actually a list, so that other such flags can be passed in the future (universes, guard condition…).

1 files changed, 16 insertions, 2 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index be11b86adb..25e679ba8c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -71,6 +71,14 @@ let make_bullet s =
   | '*' -> Star n
   | _ -> assert false
 
+type nl_assumption =
+  | Positive
+let eq_nl_assumption x y =
+  match x,y with
+  | Positive,Positive -> true
+let check_positivity l =
+  not (List.mem_f eq_nl_assumption Positive l)
+
 let default_command_entry =
   Gram.Entry.of_parser "command_entry"
     (fun strm -> Gram.parse_tokens_after_filter (get_command_entry ()) strm)
@@ -200,11 +208,11 @@ GEXTEND Gram
       | IDENT "Let"; id = identref; b = def_body ->
           VernacDefinition ((Some Discharge, Definition), id, b)
       (* Gallina inductive declarations *)
-      | priv = private_token; f = finite_token;
+      | priv = private_token; a = assume_token; f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
 	  let (k,f) = f in
 	  let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
-          VernacInductive (true,priv,f,indl)
+          VernacInductive (check_positivity a,priv,f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           VernacFixpoint (None, recs)
       | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
@@ -269,6 +277,12 @@ GEXTEND Gram
       | IDENT "Structure" -> (Structure,BiFinite)
       | IDENT "Class" -> (Class true,BiFinite) ] ]
   ;
+  assume_token:
+    [ [ IDENT "Assume"; "[" ; l=LIST1 nl_assumption ; "]" -> l | -> [] ] ]
+  ;
+  nl_assumption:
+    [ [ IDENT "Positive" -> Positive ] ]
+  ;
   private_token:
     [ [ IDENT "Private" -> true | -> false ] ]
   ;