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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \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 Names
open Constr
open Mod_subst
(*s Global reference is a kernel side type for all references together *)
type global_reference = GlobRef.t =
| VarRef of variable (** A reference to the section-context. *)
| ConstRef of Constant.t (** A reference to the environment. *)
| IndRef of inductive (** A reference to an inductive type. *)
| ConstructRef of constructor (** A reference to a constructor of an inductive type. *)
let isVarRef = function VarRef _ -> true | _ -> false
let isConstRef = function ConstRef _ -> true | _ -> false
let isIndRef = function IndRef _ -> true | _ -> false
let isConstructRef = function ConstructRef _ -> true | _ -> false
let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef"
let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef"
let subst_constructor subst (ind,j as ref) =
let ind' = subst_ind subst ind in
if ind==ind' then ref
else (ind',j)
let subst_global_reference subst ref = match ref with
| VarRef var -> ref
| ConstRef kn ->
let kn' = subst_constant subst kn in
if kn==kn' then ref else ConstRef kn'
| IndRef ind ->
let ind' = subst_ind subst ind in
if ind==ind' then ref else IndRef ind'
| ConstructRef ((kn,i),j as c) ->
let c' = subst_constructor subst c in
if c'==c then ref else ConstructRef c'
let subst_global subst ref = match ref with
| VarRef var -> ref, None
| ConstRef kn ->
let kn',t = subst_con subst kn in
if kn==kn' then ref, None else ConstRef kn', t
| IndRef ind ->
let ind' = subst_ind subst ind in
if ind==ind' then ref, None else IndRef ind', None
| ConstructRef ((kn,i),j as c) ->
let c' = subst_constructor subst c in
if c'==c then ref,None else ConstructRef c', None
let canonical_gr = function
| ConstRef con -> ConstRef(Constant.make1 (Constant.canonical con))
| IndRef (kn,i) -> IndRef(MutInd.make1(MutInd.canonical kn),i)
| ConstructRef ((kn,i),j )-> ConstructRef((MutInd.make1(MutInd.canonical kn),i),j)
| VarRef id -> VarRef id
let global_of_constr c = match kind c with
| Const (sp,u) -> ConstRef sp
| Ind (ind_sp,u) -> IndRef ind_sp
| Construct (cstr_cp,u) -> ConstructRef cstr_cp
| Var id -> VarRef id
| _ -> raise Not_found
let is_global c t =
match c, kind t with
| ConstRef c, Const (c', _) -> Constant.equal c c'
| IndRef i, Ind (i', _) -> eq_ind i i'
| ConstructRef i, Construct (i', _) -> eq_constructor i i'
| VarRef id, Var id' -> Id.equal id id'
| _ -> false
let printable_constr_of_global = function
| VarRef id -> mkVar id
| ConstRef sp -> mkConst sp
| ConstructRef sp -> mkConstruct sp
| IndRef sp -> mkInd sp
module RefOrdered = Names.GlobRef.Ordered
module RefOrdered_env = Names.GlobRef.Ordered_env
module Refmap = Names.GlobRef.Map
module Refset = Names.GlobRef.Set
module Refmap_env = Names.GlobRef.Map_env
module Refset_env = Names.GlobRef.Set_env
(* Extended global references *)
type syndef_name = KerName.t
type extended_global_reference =
| TrueGlobal of global_reference
| SynDef of syndef_name
(* We order [extended_global_reference] via their user part
(cf. pretty printer) *)
module ExtRefOrdered = struct
type t = extended_global_reference
let equal x y =
x == y ||
match x, y with
| TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.equal rx ry
| SynDef knx, SynDef kny -> KerName.equal knx kny
| (TrueGlobal _ | SynDef _), _ -> false
let compare x y =
if x == y then 0
else match x, y with
| TrueGlobal rx, TrueGlobal ry -> GlobRef.Ordered_env.compare rx ry
| SynDef knx, SynDef kny -> KerName.compare knx kny
| TrueGlobal _, SynDef _ -> -1
| SynDef _, TrueGlobal _ -> 1
open Hashset.Combine
let hash = function
| TrueGlobal gr -> combinesmall 1 (GlobRef.Ordered_env.hash gr)
| SynDef kn -> combinesmall 2 (KerName.hash kn)
end
type global_reference_or_constr =
| IsGlobal of global_reference
| IsConstr of constr
(* Deprecated *)
let eq_gr = GlobRef.equal
|
