package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file univGen.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
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq 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)         *)
(************************************************************************)

open Sorts
open Names
open Constr
open Univ
open UVars

type sort_context_set = (Sorts.QVar.Set.t * Univ.Level.Set.t) * Univ.Constraints.t

type 'a in_sort_context_set = 'a * sort_context_set

let empty_sort_context = (QVar.Set.empty, Level.Set.empty), Constraints.empty

let is_empty_sort_context ((qs,us),csts) =
  QVar.Set.is_empty qs && Level.Set.is_empty us && Constraints.is_empty csts

let sort_context_union ((qs,us),csts) ((qs',us'),csts') =
  ((QVar.Set.union qs qs', Level.Set.union us us'),Constraints.union csts csts')

let diff_sort_context ((qs,us),csts) ((qs',us'),csts') =
  (QVar.Set.diff qs qs', Level.Set.diff us us'), Constraints.diff csts csts'

type univ_length_mismatch = {
  actual : int * int;
  expect : int * int;
}
(* Due to an OCaml bug ocaml/ocaml#10027 inlining this record will cause
compliation with -rectypes to crash. *)
exception UniverseLengthMismatch of univ_length_mismatch

let () = CErrors.register_handler (function
    | UniverseLengthMismatch { actual=(aq,au); expect=(eq,eu) } ->
      let ppreal, ppexpected =
        if aq = 0 && eq = 0 then Pp.(int au, int eu)
        else Pp.(str "(" ++ int aq ++ str " | " ++ int au ++ str ")"
                , str "(" ++ int eq ++ str " | " ++ int eu ++ str ")")
      in
      Some Pp.(str "Universe instance length is " ++ ppreal
               ++ str " but should be " ++ ppexpected ++ str".")
  | _ -> None)

(* Generator of levels *)
let new_univ_id =
  let cnt = ref 0 in
  fun () -> incr cnt; !cnt

let new_univ_global () =
  let s = if Flags.async_proofs_is_worker() then !Flags.async_proofs_worker_id else "" in
  Univ.UGlobal.make (Global.current_dirpath ()) s (new_univ_id ())

let fresh_level () =
  Univ.Level.make (new_univ_global ())

let new_sort_id =
  let cnt = ref 0 in
  fun () -> incr cnt; !cnt

let new_sort_global () =
  let s = if Flags.async_proofs_is_worker() then !Flags.async_proofs_worker_id else "" in
  Sorts.QVar.make_unif s (new_sort_id ())

let fresh_instance auctx : _ in_sort_context_set =
  let qlen, ulen = AbstractContext.size auctx in
  let qinst = Array.init qlen (fun _ -> Sorts.Quality.QVar (new_sort_global())) in
  let uinst = Array.init ulen (fun _ -> fresh_level()) in
  let qctx = Array.fold_left (fun qctx q -> match q with
      | Sorts.Quality.QVar q -> Sorts.QVar.Set.add q qctx
      | _ -> assert false)
      Sorts.QVar.Set.empty
      qinst
  in
  let uctx = Array.fold_right Level.Set.add uinst Level.Set.empty in
  let inst = Instance.of_array (qinst,uinst) in
  inst, ((qctx,uctx), AbstractContext.instantiate inst auctx)

let existing_instance ?loc auctx inst =
  let () =
    let actual = Instance.length inst
    and expect = AbstractContext.size auctx in
      if not (UVars.eq_sizes actual expect) then
        Loc.raise ?loc (UniverseLengthMismatch { actual; expect })
      else ()
  in
  inst, ((Sorts.QVar.Set.empty,Level.Set.empty), AbstractContext.instantiate inst auctx)

let fresh_instance_from ?loc ctx = function
  | Some inst -> existing_instance ?loc ctx inst
  | None -> fresh_instance ctx

(** Fresh universe polymorphic construction *)

let fresh_global_instance ?loc ?names env gr =
  let auctx = Environ.universes_of_global env gr in
  let u, ctx = fresh_instance_from ?loc auctx names in
  u, ctx

let fresh_constant_instance env c =
  let u, ctx = fresh_global_instance env (GlobRef.ConstRef c) in
  (c, u), ctx

let fresh_inductive_instance env ind =
  let u, ctx = fresh_global_instance env (GlobRef.IndRef ind) in
  (ind, u), ctx

let fresh_constructor_instance env c =
  let u, ctx = fresh_global_instance env (GlobRef.ConstructRef c) in
  (c, u), ctx

let fresh_array_instance env =
  let auctx = CPrimitives.typ_univs CPrimitives.PT_array in
  let u, ctx = fresh_instance_from auctx None in
  u, ctx

let fresh_global_instance ?loc ?names env gr =
  let u, ctx = fresh_global_instance ?loc ?names env gr in
  mkRef (gr, u), ctx

let constr_of_monomorphic_global env gr =
  if not (Environ.is_polymorphic env gr) then
    fst (fresh_global_instance env gr)
  else CErrors.user_err
      Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++
          str " would forget universes.")

let fresh_sort_in_family = function
  | InSProp -> Sorts.sprop, empty_sort_context
  | InProp -> Sorts.prop, empty_sort_context
  | InSet -> Sorts.set, empty_sort_context
  | InType | InQSort (* Treat as Type *) ->
    let u = fresh_level () in
      sort_of_univ (Univ.Universe.make u), ((QVar.Set.empty,Level.Set.singleton u),Constraints.empty)

let new_global_univ () =
  let u = fresh_level () in
  (Univ.Universe.make u, ContextSet.singleton u)

let fresh_universe_context_set_instance ctx =
  if ContextSet.is_empty ctx then Level.Map.empty, ctx
  else
    let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in
    let univs',subst = Level.Set.fold
      (fun u (univs',subst) ->
        let u' = fresh_level () in
          (Level.Set.add u' univs', Level.Map.add u u' subst))
      univs (Level.Set.empty, Level.Map.empty)
    in
    let cst' = subst_univs_level_constraints subst cst in
      subst, (univs', cst')

let fresh_sort_context_instance ((qs,us),csts) =
  let usubst, (us, csts) = fresh_universe_context_set_instance (us,csts) in
  let qsubst, qs = QVar.Set.fold (fun q (qsubst,qs) ->
      let q' = new_sort_global () in
      QVar.Map.add q (Sorts.Quality.QVar q') qsubst, QVar.Set.add q' qs)
      qs
      (QVar.Map.empty, QVar.Set.empty)
  in
  (qsubst, usubst), ((qs, us), csts)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct