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
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(* $Id$ *)
open Pp
open Util
open Names
open Term
type substitution_domain = MSI of mod_self_id | MBI of mod_bound_id
let string_of_subst_domain = function
MSI msid -> debug_string_of_msid msid
| MBI mbid -> debug_string_of_mbid mbid
module Umap = Map.Make(struct
type t = substitution_domain
let compare = Pervasives.compare
end)
(* this is correct under the condition that bound and struct
identifiers can never be identical (i.e. get the same stamp)! *)
type substitution = module_path Umap.t
let empty_subst = Umap.empty
let add_msid sid = Umap.add (MSI sid)
let add_mbid bid = Umap.add (MBI bid)
let map_msid msid mp = add_msid msid mp empty_subst
let map_mbid mbid mp = add_mbid mbid mp empty_subst
let list_contents sub =
let one_pair uid mp l =
(string_of_subst_domain uid, string_of_mp mp)::l
in
Umap.fold one_pair sub []
let debug_string_of_subst sub =
let l = List.map (fun (s1,s2) -> s1^"|->"^s2) (list_contents sub) in
"{" ^ String.concat "; " l ^ "}"
let debug_pr_subst sub =
let l = list_contents sub in
let f (s1,s2) = hov 2 (str s1 ++ spc () ++ str "|-> " ++ str s2)
in
str "{" ++ hov 2 (prlist_with_sep pr_coma f l) ++ str "}"
let rec subst_mp sub mp = (* 's like subst *)
match mp with
| MPself sid ->
(try Umap.find (MSI sid) sub with Not_found -> mp)
| MPbound bid ->
(try Umap.find (MBI bid) sub with Not_found -> mp)
| MPdot (mp1,l) ->
let mp1' = subst_mp sub mp1 in
if mp1==mp1' then
mp
else
MPdot (mp1',l)
| _ -> mp
let join subst1 subst2 =
let subst = Umap.map (subst_mp subst2) subst1 in
Umap.fold Umap.add subst2 subst
let rec occur_in_path uid path =
match uid,path with
| MSI sid,MPself sid' -> sid = sid'
| MBI bid,MPbound bid' -> bid = bid'
| _,MPdot (mp1,_) -> occur_in_path uid mp1
| _ -> false
let occur_uid uid sub =
let check_one uid' mp =
if uid = uid' || occur_in_path uid mp then raise Exit
in
try
Umap.iter check_one sub;
false
with Exit -> true
let occur_msid uid = occur_uid (MSI uid)
let occur_mbid uid = occur_uid (MBI uid)
type 'a lazy_subst =
| LSval of 'a
| LSlazy of substitution * 'a
type 'a substituted = 'a lazy_subst ref
let from_val a = ref (LSval a)
let force fsubst r =
match !r with
| LSval a -> a
| LSlazy(s,a) ->
let a' = fsubst s a in
r := LSval a';
a'
let subst_substituted s r =
match !r with
| LSval a -> ref (LSlazy(s,a))
| LSlazy(s',a) ->
let s'' = join s' s in
ref (LSlazy(s'',a))
let subst_kn sub kn =
let mp,dir,l = repr_kn kn in
let mp' = subst_mp sub mp in
if mp==mp' then kn else make_kn mp' dir l
let subst_con sub con =
let mp,dir,l = repr_con con in
let mp' = subst_mp sub mp in
if mp==mp' then con else make_con mp' dir l
let subst_evaluable_reference subst = function
| EvalVarRef id -> EvalVarRef id
| EvalConstRef kn -> EvalConstRef (subst_con subst kn)
(*
map_kn : (kernel_name -> kernel_name) -> constr -> constr
This should be rewritten to prevent duplication of constr's when not
necessary.
For now, it uses map_constr and is rather ineffective
*)
let rec map_kn f f_con c =
let func = map_kn f f_con in
match kind_of_term c with
| Const kn ->
mkConst (f_con kn)
| Ind (kn,i) ->
mkInd (f kn,i)
| Construct ((kn,i),j) ->
mkConstruct ((f kn,i),j)
| Case (ci,p,c,l) ->
let ci' = { ci with ci_ind = let (kn,i) = ci.ci_ind in f kn, i } in
mkCase (ci', func p, func c, array_smartmap func l)
| _ -> map_constr func c
let subst_mps sub =
map_kn (subst_kn sub) (subst_con sub)
|
