1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: mod_subst.ml 11924 2009-02-13 13:51:54Z soubiran $ *)
16
(* WARNING: not every constant in the associative list domain used to exist
17
in the environment. This allows a simple implementation of the join
18
operation. However, iterating over the associative list becomes a non-sense
20
type resolver = (constant * constr option) list
22
let make_resolver resolve = resolve
24
let apply_opt_resolver resolve kn =
28
try List.assoc kn resolve with Not_found -> None
30
type substitution_domain =
35
let string_of_subst_domain = function
36
MSI msid -> debug_string_of_msid msid
37
| MBI mbid -> debug_string_of_mbid mbid
38
| MPI mp -> string_of_mp mp
40
module Umap = Map.Make(struct
41
type t = substitution_domain
42
let compare = Pervasives.compare
45
type substitution = (module_path * resolver option) Umap.t
47
let empty_subst = Umap.empty
49
let add_msid msid mp =
50
Umap.add (MSI msid) (mp,None)
51
let add_mbid mbid mp resolve =
52
Umap.add (MBI mbid) (mp,resolve)
54
Umap.add (MPI mp1) (mp2,None)
57
let map_msid msid mp = add_msid msid mp empty_subst
58
let map_mbid mbid mp resolve = add_mbid mbid mp resolve empty_subst
59
let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst
61
let list_contents sub =
62
let one_pair uid (mp,_) l =
63
(string_of_subst_domain uid, string_of_mp mp)::l
65
Umap.fold one_pair sub []
67
let debug_string_of_subst sub =
68
let l = List.map (fun (s1,s2) -> s1^"|->"^s2) (list_contents sub) in
69
"{" ^ String.concat "; " l ^ "}"
71
let debug_pr_subst sub =
72
let l = list_contents sub in
73
let f (s1,s2) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2)
75
str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}"
78
let subst_mp0 sub mp = (* 's like subst *)
82
let mp',resolve = Umap.find (MSI sid) sub in
85
let mp',resolve = Umap.find (MBI bid) sub in
87
| MPdot (mp1,l) as mp2 ->
90
let mp',resolve = Umap.find (MPI mp2) sub in
93
let mp1',resolve = aux mp1 in
94
MPdot (mp1',l),resolve
96
| _ -> raise Not_found
100
with Not_found -> None
102
let subst_mp sub mp =
103
match subst_mp0 sub mp with
105
| Some (mp',_) -> mp'
108
let subst_kn0 sub kn =
109
let mp,dir,l = repr_kn kn in
110
match subst_mp0 sub mp with
112
Some (make_kn mp' dir l)
115
let subst_kn sub kn =
116
match subst_kn0 sub kn with
120
let subst_con sub con =
121
let mp,dir,l = repr_con con in
122
match subst_mp0 sub mp with
123
None -> con,mkConst con
124
| Some (mp',resolve) ->
125
let con' = make_con mp' dir l in
126
match apply_opt_resolver resolve con with
127
None -> con',mkConst con'
130
let subst_con0 sub con =
131
let mp,dir,l = repr_con con in
132
match subst_mp0 sub mp with
134
| Some (mp',resolve) ->
135
let con' = make_con mp' dir l in
136
match apply_opt_resolver resolve con with
137
None -> Some (mkConst con')
140
(* Here the semantics is completely unclear.
141
What does "Hint Unfold t" means when "t" is a parameter?
142
Does the user mean "Unfold X.t" or does she mean "Unfold y"
143
where X.t is later on instantiated with y? I choose the first
144
interpretation (i.e. an evaluable reference is never expanded). *)
145
let subst_evaluable_reference subst = function
146
| EvalVarRef id -> EvalVarRef id
147
| EvalConstRef kn -> EvalConstRef (fst (subst_con subst kn))
151
let rec map_kn f f' c =
152
let func = map_kn f f' in
153
match kind_of_term c with
157
| Some const ->const)
163
| Construct ((kn,i),j) ->
167
mkConstruct ((kn',i),j))
168
| Case (ci,p,ct,l) ->
170
let (kn,i) = ci.ci_ind in
171
(match f kn with None -> ci.ci_ind | Some kn' -> kn',i ) in
174
let l' = array_smartmap func l in
175
if (ci.ci_ind==ci_ind && p'==p
176
&& l'==l && ct'==ct)then c
178
mkCase ({ci with ci_ind = ci_ind},
183
if (t'==t && ct'==ct) then c
184
else mkCast (ct', k, t')
188
if (t'==t && ct'==ct) then c
189
else mkProd (na, t', ct')
190
| Lambda (na,t,ct) ->
193
if (t'==t && ct'==ct) then c
194
else mkLambda (na, t', ct')
195
| LetIn (na,b,t,ct) ->
199
if (t'==t && ct'==ct && b==b') then c
200
else mkLetIn (na, b', t', ct')
203
let l' = array_smartmap func l in
204
if (ct'== ct && l'==l) then c
207
let l' = array_smartmap func l in
210
| Fix (ln,(lna,tl,bl)) ->
211
let tl' = array_smartmap func tl in
212
let bl' = array_smartmap func bl in
213
if (bl == bl'&& tl == tl') then c
214
else mkFix (ln,(lna,tl',bl'))
215
| CoFix(ln,(lna,tl,bl)) ->
216
let tl' = array_smartmap func tl in
217
let bl' = array_smartmap func bl in
218
if (bl == bl'&& tl == tl') then c
219
else mkCoFix (ln,(lna,tl',bl'))
223
map_kn (subst_kn0 sub) (subst_con0 sub)
225
let rec replace_mp_in_mp mpfrom mpto mp =
227
| _ when mp = mpfrom -> mpto
229
let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
234
let replace_mp_in_con mpfrom mpto kn =
235
let mp,dir,l = repr_con kn in
236
let mp'' = replace_mp_in_mp mpfrom mpto mp in
238
else make_con mp'' dir l
240
exception BothSubstitutionsAreIdentitySubstitutions
241
exception ChangeDomain of resolver
243
let join (subst1 : substitution) (subst2 : substitution) =
244
let apply_subst (sub : substitution) key (mp,resolve) =
246
match subst_mp0 sub mp with
248
| Some (mp',resolve') -> mp',resolve' in
249
let resolve'' : resolver option =
255
None -> raise BothSubstitutionsAreIdentitySubstitutions
256
| Some res -> raise (ChangeDomain res) end
267
let kn' = replace_mp_in_con (MPself msid) mp kn in
268
apply_opt_resolver resolve' kn'
270
let kn' = replace_mp_in_con (MPbound mbid) mp kn in
271
apply_opt_resolver resolve' kn'
273
let kn' = replace_mp_in_con mp1 mp kn in
274
apply_opt_resolver resolve' kn')
275
| Some t -> Some (subst_mps sub t)) res)
277
BothSubstitutionsAreIdentitySubstitutions -> None
278
| ChangeDomain res ->
279
let rec changeDom = function
284
MSI msid -> MPself msid
285
| MBI mbid -> MPbound mbid
287
let kn' = replace_mp_in_con mp key' kn in
289
(*the key does not appear in kn, we remove it
290
from the resolver that we are building*)
293
(kn',topt)::(changeDom r)
298
let subst = Umap.mapi (apply_subst subst2) subst1 in
299
(Umap.fold Umap.add subst2 subst)
301
let subst_key subst1 subst2 =
302
let replace_in_key key (mp,resolve) sub=
307
match subst_mp0 subst1 mp1 with
309
| Some (mp2,_) -> Some (MPI mp2)
314
| None -> Umap.add key (mp,resolve) sub
315
| Some mpi -> Umap.add mpi (mp,resolve) sub
317
Umap.fold replace_in_key subst2 empty_subst
319
let update_subst_alias subst1 subst2 =
320
let subst_inv key (mp,resolve) sub =
323
| MBI msid -> MPbound msid
324
| MSI msid -> MPself msid
328
| MPbound mbid -> Umap.add (MBI mbid) (newmp,None) sub
329
| MPself msid -> Umap.add (MSI msid) (newmp,None) sub
330
| _ -> Umap.add (MPI mp) (newmp,None) sub
332
let subst_mbi = Umap.fold subst_inv subst2 empty_subst in
333
let alias_subst key (mp,resolve) sub=
338
match subst_mp0 subst_mbi mp1 with
340
| Some (mp2,_) -> Some (MPI mp2)
345
| None -> Umap.add key (mp,resolve) sub
346
| Some mpi -> Umap.add mpi (mp,resolve) sub
348
Umap.fold alias_subst subst1 empty_subst
350
let update_subst subst1 subst2 =
351
let subst_inv key (mp,resolve) l =
354
| MBI msid -> MPbound msid
355
| MSI msid -> MPself msid
359
| MPbound mbid -> ((MBI mbid),newmp,resolve)::l
360
| MPself msid -> ((MSI msid),newmp,resolve)::l
361
| _ -> ((MPI mp),newmp,resolve)::l
363
let subst_mbi = Umap.fold subst_inv subst2 [] in
364
let alias_subst key (mp,resolve) sub=
368
let compute_set_newkey l (k,mp',resolve) =
369
let mp_from_key = match k with
370
| MBI msid -> MPbound msid
371
| MSI msid -> MPself msid
374
let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in
375
if new_mp1 == mp1 then l else (MPI new_mp1,resolve)::l
378
match List.fold_left compute_set_newkey [] subst_mbi with
387
List.fold_left (fun s (k,r) -> Umap.add k (mp,r) s)
390
Umap.fold alias_subst subst1 empty_subst
392
let join_alias (subst1 : substitution) (subst2 : substitution) =
393
let apply_subst (sub : substitution) key (mp,resolve) =
395
match subst_mp0 sub mp with
397
| Some (mp',resolve') -> mp',resolve' in
398
let resolve'' : resolver option =
405
None -> raise BothSubstitutionsAreIdentitySubstitutions
406
| Some res -> raise (ChangeDomain res)
416
let kn' = replace_mp_in_con (MPself msid) mp kn in
417
apply_opt_resolver resolve' kn'
419
let kn' = replace_mp_in_con (MPbound mbid) mp kn in
420
apply_opt_resolver resolve' kn'
422
let kn' = replace_mp_in_con mp1 mp kn in
423
apply_opt_resolver resolve' kn')
424
| Some t -> Some (subst_mps sub t)) res)
426
BothSubstitutionsAreIdentitySubstitutions -> None
427
| ChangeDomain res ->
428
let rec changeDom = function
433
MSI msid -> MPself msid
434
| MBI mbid -> MPbound mbid
436
let kn' = replace_mp_in_con mp key' kn in
438
(*the key does not appear in kn, we remove it
439
from the resolver that we are building*)
442
(kn',topt)::(changeDom r)
447
Umap.mapi (apply_subst subst2) subst1
449
let remove_alias subst =
450
let rec remove key (mp,resolve) sub =
453
| _ -> Umap.add key (mp,resolve) sub
455
Umap.fold remove subst empty_subst
458
let rec occur_in_path uid path =
460
| MSI sid,MPself sid' -> sid = sid'
461
| MBI bid,MPbound bid' -> bid = bid'
462
| _,MPdot (mp1,_) -> occur_in_path uid mp1
465
let occur_uid uid sub =
466
let check_one uid' (mp,_) =
467
if uid = uid' || occur_in_path uid mp then raise Exit
470
Umap.iter check_one sub;
474
let occur_msid uid = occur_uid (MSI uid)
475
let occur_mbid uid = occur_uid (MBI uid)
479
| LSlazy of substitution * 'a
481
type 'a substituted = 'a lazy_subst ref
483
let from_val a = ref (LSval a)
489
let a' = fsubst s a in
493
let subst_substituted s r =
495
| LSval a -> ref (LSlazy(s,a))
497
let s'' = join s' s in
added
removed
kernel/mod_subst.ml
