From afe5d78e85bc276a7a9b1386f504c98b02454463 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 16 May 2018 15:22:35 +0200 Subject: dev/doc/univpoly.{txt => md}, split off primitive projection info --- dev/doc/primproj.md | 41 ++++++++ dev/doc/universes.md | 226 ++++++++++++++++++++++++++++++++++++++++ dev/doc/universes.txt | 26 ----- dev/doc/univpoly.txt | 279 -------------------------------------------------- 4 files changed, 267 insertions(+), 305 deletions(-) create mode 100644 dev/doc/primproj.md create mode 100644 dev/doc/universes.md delete mode 100644 dev/doc/universes.txt delete mode 100644 dev/doc/univpoly.txt (limited to 'dev/doc') diff --git a/dev/doc/primproj.md b/dev/doc/primproj.md new file mode 100644 index 000000000..ea76aeeab --- /dev/null +++ b/dev/doc/primproj.md @@ -0,0 +1,41 @@ +Primitive Projections +--------------------- + + | Proj of Projection.t * constr + +Projections are always applied to a term, which must be of a record +type (i.e. reducible to an inductive type `I params`). Type-checking, +reduction and conversion are fast (not as fast as they could be yet) +because we don't keep parameters around. As you can see, it's +currently a `constant` that is used here to refer to the projection, +that will change to an abstract `projection` type in the future. +Basically a projection constant records which inductive it is a +projection for, the number of params and the actual position in the +constructor that must be projected. For compatibility reason, we also +define an eta-expanded form (accessible from user syntax `@f`). The +constant_entry of a projection has both informations. Declaring a +record (under `Set Primitive Projections`) will generate such +definitions. The API to declare them is not stable at the moment, but +the inductive type declaration also knows about the projections, i.e. +a record inductive type decl contains an array of terms representing +the projections. This is used to implement eta-conversion for record +types (with at least one field and having all projections definable). +The canonical value being `Build_R (pn x) ... (pn x)`. Unification and +conversion work up to this eta rule. The records can also be universe +polymorphic of course, and we don't need to keep track of the universe +instance for the projections either. Projections are reduced _eagerly_ +everywhere, and introduce a new `Zproj` constructor in the abstract +machines that obeys both the delta (for the constant opacity) and iota +laws (for the actual reduction). Refolding works as well (afaict), but +there is a slight hack there related to universes (not projections). + +For the ML programmer, the biggest change is that pattern-matchings on +kind_of_term require an additional case, that is handled usually +exactly like an `App (Const p) arg`. + +There are slight hacks related to hints is well, to use the primitive +projection form of f when one does `Hint Resolve f`. Usually hint +resolve will typecheck the term, resulting in a partially applied +projection (disallowed), so we allow it to take +`constr_or_global_reference` arguments instead and special-case on +projections. Other tactic extensions might need similar treatment. diff --git a/dev/doc/universes.md b/dev/doc/universes.md new file mode 100644 index 000000000..c276603ed --- /dev/null +++ b/dev/doc/universes.md @@ -0,0 +1,226 @@ +Notes on universe polymorphism +------------------------------ + +The implementation of universe polymorphism introduces a few changes +to the API of Coq. First and foremost, the term language changes, as +global references now carry a universe level substitution: + +~~~ocaml +type 'a puniverses = 'a * Univ.Instance.t +type pconstant = constant puniverses +type pinductive = inductive puniverses +type pconstructor = constructor puniverses + +type constr = ... + | Const of puniverses + | Ind of pinductive + | Constr of pconstructor +~~~ + +Universes +--------- + +Universe instances (an array of levels) gets substituted when +unfolding definitions, are used to typecheck and are unified according +to the rules in the ITP'14 paper on universe polymorphism in Coq. + +~~~ocaml +type Level.t = Set | Prop | Level of int * dirpath (* hashconsed *) +type Instance.t = Level.t array +type Universe.t = Level.t list (* hashconsed *) +~~~ + +The universe module defines modules and abstract types for levels, +universes etc.. Structures are hashconsed (with a hack to take care +of the fact that deserialization breaks sharing). + + Definitions (constants, inductives) now carry around not only +constraints but also the universes they introduced (a Univ.UContext.t). +There is another kind of contexts `Univ.ContextSet.t`, the latter has +a set of universes, while the former has serialized the levels in an +array, and is used for polymorphic objects. Both have "reified" +constraints depending on global and local universes. + + A polymorphic definition is abstract w.r.t. the variables in this +context, while a monomorphic one (or template polymorphic) just adds the +universes and constraints to the global universe context when it is put +in the environment. No other universes than the global ones and the +declared local ones are needed to check a declaration, hence the kernel +does not produce any constraints anymore, apart from module +subtyping.... There are hence two conversion functions now: `check_conv` +and `infer_conv`: the former just checks the definition in the current env +(in which we usually push_universe_context of the associated context), +and `infer_conv` which produces constraints that were not implied by the +ambient constraints. Ideally, that one could be put out of the kernel, +but currently module subtyping needs it. + + Inference of universes is now done during refinement, and the evar_map +carries the incrementally built universe context, starting from the +global universe constraints (see `Evd.from_env`). `Evd.conversion` is a +wrapper around `infer_conv` that will do the bookkeeping for you, it +uses `evar_conv_x`. There is a universe substitution being built +incrementally according to the constraints, so one should normalize at +the end of a proof (or during a proof) with that substitution just like +we normalize evars. There are some nf_* functions in +library/universes.ml to do that. Additionally, there is a minimization +algorithm in there that can be applied at the end of a proof to simplify +the universe constraints used in the term. It is heuristic but +validity-preserving. No user-introduced universe (i.e. coming from a +user-written anonymous Type) gets touched by this, only the fresh +universes generated for each global application. Using +~~~ocaml +val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic +~~~ +Is the way to make a constr out of a global reference in the new API. +If they constr is polymorphic, it will add the necessary constraints to +the evar_map. Even if a constr is not polymorphic, we have to take care +of keeping track of its universes. Typically, using: +~~~ocaml + mkApp (coq_id_function, [| A; a |]) +~~~ +and putting it in a proof term is not enough now. One has to somehow +show that A's type is in cumululativity relation with id's type +argument, incurring a universe constraint. To do this, one can simply +call Typing.resolve_evars env evdref c which will do some infer_conv to +produce the right constraints and put them in the evar_map. Of course in +some cases you might know from an invariant that no new constraint would +be produced and get rid of it. Anyway the kernel will tell you if you +forgot some. As a temporary way out, `Universes.constr_of_global` allows +you to make a constr from any non-polymorphic constant, but it will fail +on polymorphic ones. + +Other than that, unification (w_unify and evarconv) now take account of universes and +produce only well-typed evar_maps. + +Some syntactic comparisons like the one used in `change` have to be +adapted to allow identification up-to-universes (when dealing with +polymorphic references), `make_eq_univs_test` is there to help. +In constr, there are actually many new comparison functions to deal with +that: +~~~ocaml +(** [equal a b] is true if [a] equals [b] modulo alpha, casts, + and application grouping *) +val equal : constr -> constr -> bool + +(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, + application grouping and the universe equalities in [u]. *) +val eq_constr_univs : constr Univ.check_function + +(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo + alpha, casts, application grouping and the universe inequalities in [u]. *) +val leq_constr_univs : constr Univ.check_function + +(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, + application grouping and the universe equalities in [c]. *) +val eq_constr_universes : constr -> constr -> bool Univ.universe_constrained + +(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo + alpha, casts, application grouping and the universe inequalities in [c]. *) +val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained + +(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, + application grouping and ignoring universe instances. *) +val eq_constr_nounivs : constr -> constr -> bool +~~~ +The `_univs` versions are doing checking of universe constraints +according to a graph, while the `_universes` are producing (non-atomic) +universe constraints. The non-atomic universe constraints include the +`ULub` constructor: when comparing `f (* u1 u2 *) c` and `f (* u1' u2' +*) c` we add ULub constraints on `u1, u1'` and `u2, u2'`. These are +treated specially: as unfolding `f` might not result in these +unifications, we need to keep track of the fact that failure to satisfy +them does not mean that the term are actually equal. This is used in +unification but probably not necessary to the average programmer. + +Another issue for ML programmers is that tables of constrs now usually +need to take a `constr Univ.in_universe_context_set` instead, and +properly refresh the universes context when using the constr, e.g. using +Clenv.refresh_undefined_univs clenv or: +~~~ocaml +(** Get fresh variables for the universe context. + Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) +val fresh_universe_context_set_instance : universe_context_set -> + universe_level_subst * universe_context_set +~~~ +The substitution should be applied to the constr(s) under consideration, +and the context_set merged with the current evar_map with: +~~~ocaml +val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map +~~~ +The `rigid` flag here should be `Evd.univ_flexible` most of the +time. This means the universe levels of polymorphic objects in the +constr might get instantiated instead of generating equality constraints +(Evd.univ_rigid does that). + +On this issue, I recommend forcing commands to take `global_reference`s +only, the user can declare his specialized terms used as hints as +constants and this is cleaner. Alas, backward-compatibility-wise, +this is the only solution I found. In the case of global_references +only, it's just a matter of using `Evd.fresh_global` / +`pf_constr_of_global` to let the system take care of universes. + + +The universe graph +------------------ + +To accomodate universe polymorphic definitions, the graph structure in +kernel/univ.ml was modified. The new API forces every universe to be +declared before it is mentionned in any constraint. This forces to +declare every universe to be >= Set or > Set. Every universe variable +introduced during elaboration is >= Set. Every _global_ universe is now +declared explicitly > Set, _after_ typechecking the definition. In +polymorphic definitions Type@{i} ranges over Set and any other universe +j. However, at instantiation time for polymorphic references, one can +try to instantiate a universe parameter with Prop as well, if the +instantiated constraints allow it. The graph invariants ensure that +no universe i can be set lower than Set, so the chain of universes +always bottoms down at Prop < Set. + +Modules +------- + +One has to think of universes in modules as being globally declared, so +when including a module (type) which declares a type i (e.g. through a +parameter), we get back a copy of i and not some fresh universe. + +Incompatibilities +----------------- + +Old-style universe polymorphic definitions were implemented by taking +advantage of the fact that elaboration (i.e., pretyping and unification) +were _not_ universe aware, so some of the constraints generated during +pretypechecking would be forgotten. In the current setting, this is not +possible, as unification ensures that the substitution is built is +entirely well-typed, even w.r.t universes. This means that some terms +that type-checked before no longer do, especially projections of the +pair: +~~~coq +@fst ?x ?y : prod ?x ?y : Type (max(Datatypes.i, Datatypes.j)). +~~~ +The "template universe polymorphic" variables i and j appear during +typing without being refreshed, meaning that they can be lowered (have +upper constraints) with user-introduced universes. In most cases this +won't work, so ?x and ?y have to be instantiated earlier, either from +the type of the actual projected pair term (some t : prod A B) or the +typing constraint. Adding the correct type annotations will always fix +this. + + +Unification semantics +--------------------- + +In Ltac, matching with: + +- a universe polymorphic constant `c` matches any instance of the + constant. +- a variable ?x already bound to a term `t` (non-linear pattern) uses + strict equality of universes (e.g., Type@{i} and Type@{j} are not + equal). + +In tactics: + +- `change foo with bar`, `pattern foo` will unify all instances of `foo` + (and convert them with `bar`). This might incur unifications of + universes. `change` uses conversion while `pattern` only does + syntactic matching up-to unification of universes. +- `apply`, `refine` use unification up to universes. diff --git a/dev/doc/universes.txt b/dev/doc/universes.txt deleted file mode 100644 index a40706e99..000000000 --- a/dev/doc/universes.txt +++ /dev/null @@ -1,26 +0,0 @@ -How to debug universes? - -1. There is a command Print Universes in Coq toplevel - - Print Universes. - prints the graph of universes in the form of constraints - - Print Universes "file". - produces the "file" containing universe constraints in the form - univ1 # univ2 ; - where # can be either > >= or = - - If "file" ends with .gv or .dot, the resulting file will be in - dot format. - - - *) for dot see http://www.research.att.com/sw/tools/graphviz/ - - -2. There is a printing option - - {Set,Unset} Printing Universes. - - which, when set, makes all pretty-printed Type's annotated with the - name of the universe. - diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt deleted file mode 100644 index ca3d520c7..000000000 --- a/dev/doc/univpoly.txt +++ /dev/null @@ -1,279 +0,0 @@ -Notes on universe polymorphism and primitive projections, M. Sozeau -=================================================================== - -The new implementation of universe polymorphism and primitive -projections introduces a few changes to the API of Coq. First and -foremost, the term language changes, as global references now carry a -universe level substitution: - -type 'a puniverses = 'a * Univ.Instance.t -type pconstant = constant puniverses -type pinductive = inductive puniverses -type pconstructor = constructor puniverses - -type constr = ... - | Const of puniverses - | Ind of pinductive - | Constr of pconstructor - | Proj of constant * constr - - -Universes -========= - - Universe instances (an array of levels) gets substituted when -unfolding definitions, are used to typecheck and are unified according -to the rules in the ITP'14 paper on universe polymorphism in Coq. - -type Level.t = Set | Prop | Level of int * dirpath (* hashconsed *) -type Instance.t = Level.t array -type Universe.t = Level.t list (* hashconsed *) - -The universe module defines modules and abstract types for levels, -universes etc.. Structures are hashconsed (with a hack to take care -of the fact that deserialization breaks sharing). - - Definitions (constants, inductives) now carry around not only -constraints but also the universes they introduced (a Univ.UContext.t). -There is another kind of contexts [Univ.ContextSet.t], the latter has -a set of universes, while the former has serialized the levels in an -array, and is used for polymorphic objects. Both have "reified" -constraints depending on global and local universes. - - A polymorphic definition is abstract w.r.t. the variables in this -context, while a monomorphic one (or template polymorphic) just adds the -universes and constraints to the global universe context when it is put -in the environment. No other universes than the global ones and the -declared local ones are needed to check a declaration, hence the kernel -does not produce any constraints anymore, apart from module -subtyping.... There are hence two conversion functions now: [check_conv] -and [infer_conv]: the former just checks the definition in the current env -(in which we usually push_universe_context of the associated context), -and [infer_conv] which produces constraints that were not implied by the -ambient constraints. Ideally, that one could be put out of the kernel, -but currently module subtyping needs it. - - Inference of universes is now done during refinement, and the evar_map -carries the incrementally built universe context, starting from the -global universe constraints (see [Evd.from_env]). [Evd.conversion] is a -wrapper around [infer_conv] that will do the bookkeeping for you, it -uses [evar_conv_x]. There is a universe substitution being built -incrementally according to the constraints, so one should normalize at -the end of a proof (or during a proof) with that substitution just like -we normalize evars. There are some nf_* functions in -library/universes.ml to do that. Additionally, there is a minimization -algorithm in there that can be applied at the end of a proof to simplify -the universe constraints used in the term. It is heuristic but -validity-preserving. No user-introduced universe (i.e. coming from a -user-written anonymous Type) gets touched by this, only the fresh -universes generated for each global application. Using - -val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic - -Is the way to make a constr out of a global reference in the new API. -If they constr is polymorphic, it will add the necessary constraints to -the evar_map. Even if a constr is not polymorphic, we have to take care -of keeping track of its universes. Typically, using: - - mkApp (coq_id_function, [| A; a |]) - -and putting it in a proof term is not enough now. One has to somehow -show that A's type is in cumululativity relation with id's type -argument, incurring a universe constraint. To do this, one can simply -call Typing.resolve_evars env evdref c which will do some infer_conv to -produce the right constraints and put them in the evar_map. Of course in -some cases you might know from an invariant that no new constraint would -be produced and get rid of it. Anyway the kernel will tell you if you -forgot some. As a temporary way out, [Universes.constr_of_global] allows -you to make a constr from any non-polymorphic constant, but it will fail -on polymorphic ones. - -Other than that, unification (w_unify and evarconv) now take account of universes and -produce only well-typed evar_maps. - -Some syntactic comparisons like the one used in [change] have to be -adapted to allow identification up-to-universes (when dealing with -polymorphic references), [make_eq_univs_test] is there to help. -In constr, there are actually many new comparison functions to deal with -that: - -(** [equal a b] is true if [a] equals [b] modulo alpha, casts, - and application grouping *) -val equal : constr -> constr -> bool - -(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts, - application grouping and the universe equalities in [u]. *) -val eq_constr_univs : constr Univ.check_function - -(** [leq_constr_univs u a b] is [true] if [a] is convertible to [b] modulo - alpha, casts, application grouping and the universe inequalities in [u]. *) -val leq_constr_univs : constr Univ.check_function - -(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and the universe equalities in [c]. *) -val eq_constr_universes : constr -> constr -> bool Univ.universe_constrained - -(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo - alpha, casts, application grouping and the universe inequalities in [c]. *) -val leq_constr_universes : constr -> constr -> bool Univ.universe_constrained - -(** [eq_constr_univs a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and ignoring universe instances. *) -val eq_constr_nounivs : constr -> constr -> bool - -The [_univs] versions are doing checking of universe constraints -according to a graph, while the [_universes] are producing (non-atomic) -universe constraints. The non-atomic universe constraints include the -[ULub] constructor: when comparing [f (* u1 u2 *) c] and [f (* u1' u2' -*) c] we add ULub constraints on [u1, u1'] and [u2, u2']. These are -treated specially: as unfolding [f] might not result in these -unifications, we need to keep track of the fact that failure to satisfy -them does not mean that the term are actually equal. This is used in -unification but probably not necessary to the average programmer. - -Another issue for ML programmers is that tables of constrs now usually -need to take a [constr Univ.in_universe_context_set] instead, and -properly refresh the universes context when using the constr, e.g. using -Clenv.refresh_undefined_univs clenv or: - -(** Get fresh variables for the universe context. - Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) -val fresh_universe_context_set_instance : universe_context_set -> - universe_level_subst * universe_context_set - -The substitution should be applied to the constr(s) under consideration, -and the context_set merged with the current evar_map with: - -val merge_context_set : rigid -> evar_map -> Univ.universe_context_set -> evar_map - -The [rigid] flag here should be [Evd.univ_flexible] most of the -time. This means the universe levels of polymorphic objects in the -constr might get instantiated instead of generating equality constraints -(Evd.univ_rigid does that). - -On this issue, I recommend forcing commands to take [global_reference]s -only, the user can declare his specialized terms used as hints as -constants and this is cleaner. Alas, backward-compatibility-wise, -this is the only solution I found. In the case of global_references -only, it's just a matter of using [Evd.fresh_global] / -[pf_constr_of_global] to let the system take care of universes. - - -The universe graph -================== - -To accomodate universe polymorphic definitions, the graph structure in -kernel/univ.ml was modified. The new API forces every universe to be -declared before it is mentionned in any constraint. This forces to -declare every universe to be >= Set or > Set. Every universe variable -introduced during elaboration is >= Set. Every _global_ universe is now -declared explicitly > Set, _after_ typechecking the definition. In -polymorphic definitions Type@{i} ranges over Set and any other universe -j. However, at instantiation time for polymorphic references, one can -try to instantiate a universe parameter with Prop as well, if the -instantiated constraints allow it. The graph invariants ensure that -no universe i can be set lower than Set, so the chain of universes -always bottoms down at Prop < Set. - -Modules -======= - -One has to think of universes in modules as being globally declared, so -when including a module (type) which declares a type i (e.g. through a -parameter), we get back a copy of i and not some fresh universe. - -Projections -=========== - - | Proj of constant * constr - -Projections are always applied to a term, which must be of a record type -(i.e. reducible to an inductive type [I params]). Type-checking, -reduction and conversion are fast (not as fast as they could be yet) -because we don't keep parameters around. As you can see, it's currently -a [constant] that is used here to refer to the projection, that will -change to an abstract [projection] type in the future. Basically a -projection constant records which inductive it is a projection for, the -number of params and the actual position in the constructor that must be -projected. For compatibility reason, we also define an eta-expanded form -(accessible from user syntax @f). The constant_entry of a projection has -both informations. Declaring a record (under [Set Primitive -Projections]) will generate such definitions. The API to declare them is -not stable at the moment, but the inductive type declaration also knows -about the projections, i.e. a record inductive type decl contains an -array of terms representing the projections. This is used to implement -eta-conversion for record types (with at least one field and having all -projections definable). The canonical value being [Build_R (pn x) -... (pn x)]. Unification and conversion work up to this eta rule. The -records can also be universe polymorphic of course, and we don't need to -keep track of the universe instance for the projections either. -Projections are reduced _eagerly_ everywhere, and introduce a new Zproj -constructor in the abstract machines that obeys both the delta (for the -constant opacity) and iota laws (for the actual reduction). Refolding -works as well (afaict), but there is a slight hack there related to -universes (not projections). - -For the ML programmer, the biggest change is that pattern-matchings on -kind_of_term require an additional case, that is handled usually exactly -like an [App (Const p) arg]. - -There are slight hacks related to hints is well, to use the primitive -projection form of f when one does [Hint Resolve f]. Usually hint -resolve will typecheck the term, resulting in a partially applied -projection (disallowed), so we allow it to take -[constr_or_global_reference] arguments instead and special-case on -projections. Other tactic extensions might need similar treatment. - -WIP -=== - -- [vm_compute] does not deal with universes and projections correctly, -except when it goes to a normal form with no projections or polymorphic -constants left (the most common case). E.g. Ring with Set Universe -Polymorphism and Set Primitive Projections work (at least it did at some -point, I didn't recheck yet). - -- [native_compute] works with universes and projections. - - -Incompatibilities -================= - -Old-style universe polymorphic definitions were implemented by taking -advantage of the fact that elaboration (i.e., pretyping and unification) -were _not_ universe aware, so some of the constraints generated during -pretypechecking would be forgotten. In the current setting, this is not -possible, as unification ensures that the substitution is built is -entirely well-typed, even w.r.t universes. This means that some terms -that type-checked before no longer do, especially projections of the -pair: - -@fst ?x ?y : prod ?x ?y : Type (max(Datatypes.i, Datatypes.j)). - -The "template universe polymorphic" variables i and j appear during -typing without being refreshed, meaning that they can be lowered (have -upper constraints) with user-introduced universes. In most cases this -won't work, so ?x and ?y have to be instantiated earlier, either from -the type of the actual projected pair term (some t : prod A B) or the -typing constraint. Adding the correct type annotations will always fix -this. - - -Unification semantics -===================== - -In Ltac, matching with: - -- a universe polymorphic constant [c] matches any instance of the - constant. -- a variable ?x already bound to a term [t] (non-linear pattern) uses - strict equality of universes (e.g., Type@{i} and Type@{j} are not - equal). - -In tactics: - -- [change foo with bar], [pattern foo] will unify all instances of [foo] - (and convert them with [bar]). This might incur unifications of - universes. [change] uses conversion while [pattern] only does - syntactic matching up-to unification of universes. -- [apply], [refine] use unification up to universes. -- cgit v1.2.3