From 75508769762372043387c67a9abe94e8f940e80a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 27 Oct 2017 14:03:51 +0200 Subject: Add a non-cumulative impredicative universe SProp. Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged. --- dev/top_printers.ml | 2 ++ dev/vm_printers.ml | 1 + 2 files changed, 3 insertions(+) (limited to 'dev') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index a3d2f33216..5ece892aa2 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -306,6 +306,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; @@ -430,6 +431,7 @@ 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(); 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" -- cgit v1.2.3 From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 31 Oct 2017 17:04:02 +0100 Subject: Add relevance marks on binders. Kernel should be mostly correct, higher levels do random stuff at times. --- dev/top_printers.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'dev') diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 5ece892aa2..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 @@ -316,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" @@ -336,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) -> @@ -437,7 +438,7 @@ let print_pure_constr csr = | 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 *) -- cgit v1.2.3 From 170da77ad45cb0e504f82d075836a8f2965efe28 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 20 Dec 2018 15:58:24 +0100 Subject: Documentation for SProp --- dev/doc/SProp.md | 41 +++++++++++++++++++++++++++++++++++++++++ dev/doc/changes.md | 2 ++ 2 files changed, 43 insertions(+) create mode 100644 dev/doc/SProp.md (limited to 'dev') 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 + General deprecation - All functions marked [@@ocaml.deprecated] in 8.8 have been -- cgit v1.2.3 From d2daf895aeaa1327a33203c2f8cb7a002e3403c4 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 19 Dec 2018 15:35:34 +0100 Subject: Overlays for SProp --- dev/ci/user-overlays/08817-sprop.sh | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 dev/ci/user-overlays/08817-sprop.sh (limited to 'dev') 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 -- cgit v1.2.3