|
| 1 | +(************************************************************************) |
| 2 | +(* * The Rocq Prover / The Rocq Development Team *) |
| 3 | +(* v * Copyright INRIA, CNRS and contributors *) |
| 4 | +(* <O___,, * (see version control and CREDITS file for authors & dates) *) |
| 5 | +(* \VV/ **************************************************************) |
| 6 | +(* // * This file is distributed under the terms of the *) |
| 7 | +(* * GNU Lesser General Public License Version 2.1 *) |
| 8 | +(* * (see LICENSE file for the text of the license) *) |
| 9 | +(************************************************************************) |
| 10 | + |
| 11 | +type t = { |
| 12 | + univ_poly : bool; |
| 13 | + collapse_sort_variables : bool; |
| 14 | + cumulative : bool; |
| 15 | +} |
| 16 | + |
| 17 | +let make ~univ_poly ~collapse_sort_variables ~cumulative = |
| 18 | + if cumulative && not univ_poly then |
| 19 | + CErrors.user_err Pp.(str "Cannot have cumulative but not universe polymorphic constructions"); |
| 20 | + if not collapse_sort_variables && not univ_poly then |
| 21 | + CErrors.user_err Pp.(str "Sort metavariables must be collapsed to Type in universe monomorphic constructions"); |
| 22 | + { collapse_sort_variables; univ_poly; cumulative } |
| 23 | + |
| 24 | +let default = { collapse_sort_variables = true; univ_poly = false; cumulative = false } |
| 25 | +let of_univ_poly b = { default with univ_poly = b } |
| 26 | + |
| 27 | +let collapse_sort_variables x = x.collapse_sort_variables |
| 28 | +let univ_poly x = x.univ_poly |
| 29 | +let cumulative x = x.cumulative |
| 30 | + |
| 31 | +let pr f = |
| 32 | + let open Pp in |
| 33 | + str "{ univ_poly = " ++ bool f.univ_poly ++ spc () ++ |
| 34 | + str "; cumulative = " ++ bool f.cumulative ++ spc () ++ |
| 35 | + str "; collapse_sort_variables = " ++ bool f.collapse_sort_variables ++ spc () ++ |
| 36 | + str "}" |
| 37 | + |
| 38 | +(* Used to have distinguished default behaviors when treating assumptions/axioms, definitions or inductives *) |
| 39 | +type construction_kind = |
| 40 | + Assumption | Definition | Inductive |
0 commit comments