summaryrefslogtreecommitdiff
path: root/kernel/mod_subst.ml
blob: 6d2064bf1269f972f6e302ccc83a4aa0ac79f26b (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
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
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
(************************************************************************)
(*  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: mod_subst.ml 7538 2005-11-08 17:14:52Z herbelin $ *)

open Pp
open Util
open Names
open Term

(* WARNING: not every constant in the associative list domain used to exist
   in the environment. This allows a simple implementation of the join
   operation. However, iterating over the associative list becomes a non-sense
*)
type resolver = (constant * constr option) list

let make_resolver resolve = resolve

let apply_opt_resolver resolve kn =
 match resolve with
    None -> None
  | Some resolve ->
     try List.assoc kn resolve with Not_found -> assert false

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)

type substitution = (module_path * resolver option) Umap.t

let empty_subst = Umap.empty

let add_msid msid mp =
  Umap.add (MSI msid) (mp,None)
let add_mbid mbid mp resolve =
  Umap.add (MBI mbid) (mp,resolve)

let map_msid msid mp = add_msid msid mp empty_subst
let map_mbid mbid mp resolve = add_mbid mbid mp resolve 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 subst_mp0 sub mp = (* 's like subst *)
 let rec aux mp =
  match mp with
    | MPself sid -> 
        let mp',resolve = Umap.find (MSI sid) sub in
         mp',resolve
    | MPbound bid ->
        let mp',resolve = Umap.find (MBI bid) sub in
         mp',resolve
    | MPdot (mp1,l) -> 
	let mp1',resolve = aux mp1 in
	 MPdot (mp1',l),resolve
    | _ -> raise Not_found
 in
  try Some (aux mp) with Not_found -> None

let subst_mp sub mp =
 match subst_mp0 sub mp with
    None -> mp
  | Some (mp',_) -> mp'


let subst_kn0 sub kn =
 let mp,dir,l = repr_kn kn in
  match subst_mp0 sub mp with
     Some (mp',_) ->
      Some (make_kn mp' dir l)
   | None -> None

let subst_kn sub kn =
 match subst_kn0 sub kn with
    None -> kn
  | Some kn' -> kn'

let subst_con sub con =
 let mp,dir,l = repr_con con in
  match subst_mp0 sub mp with
     None -> con,mkConst con
   | Some (mp',resolve) ->
      let con' = make_con mp' dir l in
       match apply_opt_resolver resolve con with
          None -> con',mkConst con'
        | Some t -> con',t

(* 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). *)
let subst_evaluable_reference subst = function
  | EvalVarRef id -> EvalVarRef id
  | EvalConstRef kn -> EvalConstRef (fst (subst_con subst kn))

(* 
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' c = 
  let func = map_kn f f' in
    match kind_of_term c with
      | Const kn -> f' kn
      | Ind (kn,i) -> 
         (match f kn with
             None -> c
           | Some kn' ->
	      mkInd (kn',i))
      | Construct ((kn,i),j) -> 
         (match f kn with
             None -> c
           | Some kn' ->
	      mkConstruct ((kn',i),j))
      | Case (ci,p,c,l) ->
	  let ci' =
           { ci with
              ci_ind =
               let (kn,i) = ci.ci_ind in
                match f kn with None -> ci.ci_ind | Some kn' -> kn',i } in
	  mkCase (ci', func p, func c, array_smartmap func l) 
      | _ -> map_constr func c

let subst_mps sub = 
  map_kn (subst_kn0 sub) (fun con -> snd (subst_con sub con))

let rec replace_mp_in_mp mpfrom mpto mp =
  match mp with
    | _ when mp = mpfrom -> mpto
    | MPdot (mp1,l) -> 
	let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
	  if mp1==mp1' then mp
	  else MPdot (mp1',l)
    | _ -> mp

let replace_mp_in_con mpfrom mpto kn =
 let mp,dir,l = repr_con kn in
  let mp'' = replace_mp_in_mp mpfrom mpto mp in
    if mp==mp'' then kn
    else make_con mp'' dir l

exception BothSubstitutionsAreIdentitySubstitutions
exception ChangeDomain of resolver

let join (subst1 : substitution) (subst2 : substitution) = 
  let apply_subst (sub : substitution) key (mp,resolve) =
   let mp',resolve' =
    match subst_mp0 sub mp with
       None -> mp, None
     | Some (mp',resolve') -> mp',resolve' in
   let resolve'' : resolver option =
    try
     let res =
      match resolve with
         Some res -> res
       | None ->
          match resolve' with
             None -> raise BothSubstitutionsAreIdentitySubstitutions
           | Some res -> raise (ChangeDomain res)
     in
      Some
       (List.map
         (fun (kn,topt) ->
           kn,
           match topt with
              None ->
               (match key with
                   MSI msid ->
                    let kn' = replace_mp_in_con (MPself msid) mp kn in
                     apply_opt_resolver resolve' kn'
                 | MBI mbid ->
                    let kn' = replace_mp_in_con (MPbound mbid) mp kn in
                     apply_opt_resolver resolve' kn')
            | Some t -> Some (subst_mps sub t)) res)
    with
       BothSubstitutionsAreIdentitySubstitutions -> None
     | ChangeDomain res ->
        Some
         ((List.map
            (fun (kn,topt) ->
              let key' =
               match key with
                  MSI msid -> MPself msid
                | MBI mbid -> MPbound mbid in
              (* let's replace mp with key in kn *)
              let kn' = replace_mp_in_con mp key' kn in
               kn',topt)) res)
   in
    mp',resolve'' in
  let subst = Umap.mapi (apply_subst 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))