blob: a948d1647f274c4c28d52d17ecb93f98290888ca (
plain)
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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i $Id$ i*)
(*s [Mod_subst] *)
open Names
open Term
(* A delta_resolver maps name (constant, inductive, module_path)
to canonical name *)
type delta_resolver
type substitution
val empty_delta_resolver : delta_resolver
val add_inline_delta_resolver : constant -> delta_resolver -> delta_resolver
val add_inline_constr_delta_resolver : constant -> constr -> delta_resolver
-> delta_resolver
val add_constant_delta_resolver : constant -> delta_resolver -> delta_resolver
val add_mind_delta_resolver : mutual_inductive -> delta_resolver -> delta_resolver
val add_mp_delta_resolver : module_path -> module_path -> delta_resolver
-> delta_resolver
val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
(* Apply the substitution on the domain of the resolver *)
val subst_dom_delta_resolver : substitution -> delta_resolver -> delta_resolver
(* Apply the substitution on the codomain of the resolver *)
val subst_codom_delta_resolver : substitution -> delta_resolver -> delta_resolver
val subst_dom_codom_delta_resolver :
substitution -> delta_resolver -> delta_resolver
(* *_of_delta return the associated name of arg2 in arg1 *)
val constant_of_delta : delta_resolver -> constant -> constant
val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
val delta_of_mp : delta_resolver -> module_path -> module_path
(* Extract the set of inlined constant in the resolver *)
val inline_of_delta : delta_resolver -> kernel_name list
(* remove_mp is used for the computation of a resolver induced by Include P *)
val remove_mp_delta_resolver : delta_resolver -> module_path -> delta_resolver
(* mem tests *)
val mp_in_delta : module_path -> delta_resolver -> bool
val con_in_delta : constant -> delta_resolver -> bool
val mind_in_delta : mutual_inductive -> delta_resolver -> bool
(*substitution*)
val empty_subst : substitution
(* add_* add [arg2/arg1]{arg3} to the substitution with no
sequential composition *)
val add_mbid :
mod_bound_id -> module_path -> delta_resolver -> substitution -> substitution
val add_mp :
module_path -> module_path -> delta_resolver -> substitution -> substitution
(* map_* create a new substitution [arg2/arg1]{arg3} *)
val map_mbid :
mod_bound_id -> module_path -> delta_resolver -> substitution
val map_mp :
module_path -> module_path -> delta_resolver -> substitution
(* sequential composition:
[substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)]
*)
val join : substitution -> substitution -> substitution
type 'a substituted
val from_val : 'a -> 'a substituted
val force : (substitution -> 'a -> 'a) -> 'a substituted -> 'a
val subst_substituted : substitution -> 'a substituted -> 'a substituted
(*i debugging *)
val debug_string_of_subst : substitution -> string
val debug_pr_subst : substitution -> Pp.std_ppcmds
val debug_string_of_delta : delta_resolver -> string
val debug_pr_delta : delta_resolver -> Pp.std_ppcmds
(*i*)
(* [subst_mp sub mp] guarantees that whenever the result of the
substitution is structutally equal [mp], it is equal by pointers
as well [==] *)
val subst_mp :
substitution -> module_path -> module_path
val subst_ind :
substitution -> mutual_inductive -> mutual_inductive
val subst_kn :
substitution -> kernel_name -> kernel_name
val subst_con :
substitution -> constant -> constant * constr
(* Here the semantics is completely unclear.
What does "Hint Unfold t" means when "t" is a parameter?
Does the user mean "Unfold X.t" or does she mean "Unfold y"
where X.t is later on instantiated with y? I choose the first
interpretation (i.e. an evaluable reference is never expanded). *)
val subst_evaluable_reference :
substitution -> evaluable_global_reference -> evaluable_global_reference
(* [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *)
val replace_mp_in_kn : module_path -> module_path -> kernel_name -> kernel_name
(* [subst_mps sub c] performs the substitution [sub] on all kernel
names appearing in [c] *)
val subst_mps : substitution -> constr -> constr
(* [occur_*id id sub] returns true iff [id] occurs in [sub]
on either side *)
val occur_mbid : mod_bound_id -> substitution -> bool
|
