Source file `polyFlags.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

type t = {
  univ_poly : bool;
  collapse_sort_variables : bool;
  cumulative : bool;
}

let make ~univ_poly ~collapse_sort_variables ~cumulative =
  if cumulative && not univ_poly then
    CErrors.user_err Pp.(str "Cannot have cumulative but not universe polymorphic constructions");
  if not collapse_sort_variables && not univ_poly then
    CErrors.user_err Pp.(str "Sort metavariables must be collapsed to Type in universe monomorphic constructions");
  { collapse_sort_variables; univ_poly; cumulative }

let default = { collapse_sort_variables = true; univ_poly = false; cumulative = false }
let of_univ_poly b = { default with univ_poly = b }

let collapse_sort_variables x = x.collapse_sort_variables
let univ_poly x = x.univ_poly
let cumulative x = x.cumulative

let pr f =
  let open Pp in
  str "{ univ_poly = " ++ bool f.univ_poly ++ spc () ++
  str "; cumulative = " ++ bool f.cumulative ++ spc () ++
  str "; collapse_sort_variables = " ++ bool f.collapse_sort_variables ++ spc () ++
  str "}"

(* Used to have distinguished default behaviors when treating assumptions/axioms, definitions or inductives *)
type construction_kind =
  Assumption | Definition | Inductive