Merge PR #8817: SProp: the definitionally proof irrelevant universe

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82

5 files changed, 85 insertions, 4 deletions

diff --git a/dev/ci/user-overlays/08817-sprop.sh b/dev/ci/user-overlays/08817-sprop.sh
new file mode 100644
index 0000000000..81e18226ed
--- /dev/null
+++ b/dev/ci/user-overlays/08817-sprop.sh
@@ -0,0 +1,34 @@
+if [ "$CI_PULL_REQUEST" = "8817" ] || [ "$CI_BRANCH" = "sprop" ]; then
+    aac_tactics_CI_REF=sprop
+    aac_tactics_CI_GITURL=https://github.com/SkySkimmer/aac-tactics
+
+    coq_dpdgraph_CI_REF=sprop
+    coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph
+
+    coqhammer_CI_REF=sprop
+    coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer
+
+    elpi_CI_REF=sprop
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+    equations_CI_REF=sprop
+    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    ltac2_CI_REF=sprop
+    ltac2_CI_GITURL=https://github.com/SkySkimmer/ltac2
+
+    unicoq_CI_REF=sprop
+    unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq
+
+    mtac2_CI_REF=sprop
+    mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2
+
+    paramcoq_CI_REF=sprop
+    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+
+    quickchick_CI_REF=sprop
+    quickchick_CI_GITURL=https://github.com/SkySkimmer/QuickChick
+
+    relation_algebra_CI_REF=sprop
+    relation_algebra_CI_GITURL=https://github.com/SkySkimmer/relation-algebra
+fi
diff --git a/dev/doc/SProp.md b/dev/doc/SProp.md
new file mode 100644
index 0000000000..f263dbb867
--- /dev/null
+++ b/dev/doc/SProp.md
@@ -0,0 +1,41 @@
+# Notes on SProp
+
+(ml API side, see refman for user side)
+
+## Relevance
+
+All kernel binders (`Prod`/`Lambda`/`LetIn`/`Context` elements) are
+now annotated with a value in `type Sorts.relevance = Relevant |
+Irrelevant`. It should verify that the binder's type lives in `SProp`
+iff the annotation is `Irrelevant`.
+
+As a plugin you can generally just use `Relevant` everywhere, the
+kernel will fix it if needed when it checks the terms you produce. The
+only issue is that if you generate `Relevant` when it should have been
+`Irrelevant` you won't be able to use proof irrelevance on that
+variable until the kernel fixes it. See refman for examples as Coq
+also uses `Relevant` incorrectly in some places.
+
+This annotation is done by transforming the binder name `'a` into a
+`'a Context.binder_annot = { binder_name : 'a; binder_relevance :
+Sorts.relevance }`, eg `Prod of Name.t * types * types` becomes `Prod
+of Name.t Context.binder_annot * types * types`.
+
+If you just carry binder names around without looking at them no
+change is needed, eg if you have `match foo with Lambda (x, a, b) ->
+Prod (x, a, type_of (push_rel (LocalAssum (x,a)) env) b)`. Otherwise
+see `context.mli` for a few combinators on the `binder_annot` type.
+
+When making `Relevant` annotations you can use some convenience
+functions from `Context` (eg `annotR x = make_annot x Relevant`), also
+`mkArrowR` from `Constr`/`EConstr` which has the signature of the old
+`mkArrow`.
+
+You can enable the debug warning `bad-relevance` to help find places
+where you generate incorrect annotations.
+
+Relevance can be inferred from a well-typed term using functions in
+`Retypeops` (for `Constr`) and `Retyping` (for `EConstr`). For `x` a
+term, note the difference between its relevance as a term (is `x :
+(_ : SProp)`) and as a type (is `x : SProp`), there are functions for
+both kinds.
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 491a75bb3d..d515ec30e8 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -12,6 +12,8 @@
 
 ### ML API
 
+SProp was added, see <SProp.md>
+
 General deprecation
 
 - All functions marked [@@ocaml.deprecated] in 8.8 have been
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index a3d2f33216..0fbb0634a5 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -20,6 +20,7 @@ open Univ
 open Environ
 open Printer
 open Constr
+open Context
 open Genarg
 open Clenv
 
@@ -306,6 +307,7 @@ let constr_display csr =
     incr cnt; pp (str "with " ++ int !cnt ++ str" " ++ Level.pr u ++ fnl ())
 
   and sort_display = function
+    | SProp -> "SProp"
     | Set -> "Set"
     | Prop -> "Prop"
     | Type u -> univ_display u;
@@ -315,7 +317,7 @@ let constr_display csr =
     Array.fold_right (fun x i -> level_display x; (string_of_int !cnt)^(if not(i="")
         then (" "^i) else "")) (Instance.to_array l) ""
 
-  and name_display = function
+  and name_display x = match x.binder_name with
     | Name id -> "Name("^(Id.to_string id)^")"
     | Anonymous -> "Anonymous"
 
@@ -335,13 +337,13 @@ let print_pure_constr csr =
   | Cast (c,_, t) -> open_hovbox 1;
       print_string "("; (term_display c); print_cut();
       print_string "::"; (term_display t); print_string ")"; close_box()
-  | Prod (Name(id),t,c) ->
+  | Prod ({binder_name=Name(id)},t,c) ->
       open_hovbox 1;
       print_string"("; print_string (Id.to_string id);
       print_string ":"; box_display t;
       print_string ")"; print_cut();
       box_display c; close_box()
-  | Prod (Anonymous,t,c) ->
+  | Prod ({binder_name=Anonymous},t,c) ->
       print_string"("; box_display t; print_cut(); print_string "->";
       box_display c; print_string ")";
   | Lambda (na,t,c) ->
@@ -430,12 +432,13 @@ let print_pure_constr csr =
     Array.iter (fun u -> print_space (); pp (Level.pr u)) (Instance.to_array u)
 
   and sort_display = function
+    | SProp -> print_string "SProp"
     | Set -> print_string "Set"
     | Prop -> print_string "Prop"
     | Type u -> open_hbox();
 	print_string "Type("; pp (pr_uni u); print_string ")"; close_box()
 
-  and name_display = function
+  and name_display x = match x.binder_name with
     | Name id -> print_string (Id.to_string id)
     | Anonymous -> print_string "_"
 (* Remove the top names for library and Scratch to avoid long names *)
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index dc30793a6e..863d930968 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -25,6 +25,7 @@ let print_vfix_app () = print_string "vfix_app"
 let print_vswith () = print_string "switch"
 
 let ppsort = function
+  | SProp -> print_string "SProp"
   | Set -> print_string "Set"
   | Prop -> print_string "Prop"
   | Type u -> print_string "Type"