summaryrefslogtreecommitdiff
path: root/contrib/extraction/modutil.ml
blob: ff8daf466529bc19e00827aefab8bd0c4e1155de (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
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
(************************************************************************)
(*  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: modutil.ml 7632 2005-12-01 14:35:21Z letouzey $ i*)

open Names
open Declarations
open Environ
open Libnames
open Util
open Miniml
open Table
open Mlutil
open Mod_subst

(*S Functions upon modules missing in [Modops]. *) 

(*s Add _all_ direct subobjects of a module, not only those exported. 
   Build on the [Modops.add_signature] model. *)

let add_structure mp msb env = 
  let add_one env (l,elem) = 
    let kn = make_kn mp empty_dirpath l in 
    let con = make_con mp empty_dirpath l in 
    match elem with 
      | SEBconst cb -> Environ.add_constant con cb env 
      | SEBmind mib -> Environ.add_mind kn mib env 
      | SEBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env 
      | SEBmodtype mtb -> Environ.add_modtype kn mtb env  
  in List.fold_left add_one env msb

(*s Apply a module path substitution on a module.
   Build on the [Modops.subst_modtype] model. *)

let rec subst_module sub mb =
  let mtb' = Modops.subst_modtype sub mb.mod_type
  and meb' = option_smartmap (subst_meb sub) mb.mod_expr
  and mtb'' = option_smartmap (Modops.subst_modtype sub) mb.mod_user_type
  and mpo' = option_smartmap (subst_mp sub) mb.mod_equiv in
  if (mtb'==mb.mod_type) && (meb'==mb.mod_expr) && 
    (mtb''==mb.mod_user_type) && (mpo'==mb.mod_equiv)
  then mb
  else { mod_expr= meb'; 
	 mod_type=mtb'; 
	 mod_user_type=mtb''; 
	 mod_equiv=mpo'; 
	 mod_constraints=mb.mod_constraints }

and subst_meb sub = function 
  | MEBident mp -> MEBident (subst_mp sub mp) 
  | MEBfunctor (mbid, mtb, meb) -> 
      assert (not (occur_mbid mbid sub)); 
      MEBfunctor (mbid, Modops.subst_modtype sub mtb, subst_meb sub meb)
  | MEBstruct (msid, msb) -> 
      assert (not (occur_msid msid sub));
      MEBstruct (msid, subst_msb sub msb)
  | MEBapply (meb, meb', c) -> 
      MEBapply (subst_meb sub meb, subst_meb sub meb', c)

and subst_msb sub msb = 
  let subst_body = function
    | SEBconst cb -> SEBconst (subst_const_body sub cb)
    | SEBmind mib -> SEBmind (subst_mind sub mib)
    | SEBmodule mb -> SEBmodule (subst_module sub mb)
    | SEBmodtype mtb -> SEBmodtype (Modops.subst_modtype sub mtb)
  in List.map (fun (l,b) -> (l,subst_body b)) msb

(*s Change a msid in a module type, to follow a module expr. 
  Because of the "with" construct, the module type of a module can be a 
  [MTBsig] with a msid different from the one of the module. *)

let rec replicate_msid meb mtb = match meb,mtb with 
  | MEBfunctor (_, _, meb), MTBfunsig (mbid, mtb1, mtb2) -> 
      let mtb' = replicate_msid meb mtb2 in 
      if mtb' == mtb2 then mtb else MTBfunsig (mbid, mtb1, mtb')
  | MEBstruct (msid, _), MTBsig (msid1, msig) when msid <> msid1 -> 
      let msig' = Modops.subst_signature_msid msid1 (MPself msid) msig in
      if msig' == msig then MTBsig (msid, msig) else MTBsig (msid, msig')
  | _ -> mtb


(*S More functions concerning [module_path]. *)

let rec mp_length = function
  | MPdot (mp, _) -> 1 + (mp_length mp)
  | _ -> 1

let rec prefixes_mp mp = match mp with 
  | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp')
  | _ -> MPset.singleton mp 

let rec common_prefix prefixes_mp1 mp2 = 
  if MPset.mem mp2 prefixes_mp1 then mp2 
  else match mp2 with 
    | MPdot (mp,_) -> common_prefix prefixes_mp1 mp 
    | _ -> raise Not_found

let common_prefix_from_list mp0 mpl = 
  let prefixes_mp0 = prefixes_mp mp0 in 
  let rec f = function 
    | [] -> raise Not_found
    | mp1 :: l -> try common_prefix prefixes_mp0 mp1 with Not_found -> f l
  in f mpl

let rec modfile_of_mp mp = match mp with 
  | MPfile _ -> mp
  | MPdot (mp,_) -> modfile_of_mp mp 
  | _ -> raise Not_found

let rec parse_labels ll = function 
  | MPdot (mp,l) -> parse_labels (l::ll) mp 
  | mp -> mp,ll

let labels_of_mp mp = parse_labels [] mp 

let labels_of_ref r = 
 let mp,_,l =
  match r with
     ConstRef con -> repr_con con
   | IndRef (kn,_)
   | ConstructRef ((kn,_),_) -> repr_kn kn
   | VarRef _ -> assert false
 in
  parse_labels [l] mp

let rec add_labels_mp mp = function 
  | [] -> mp 
  | l :: ll -> add_labels_mp (MPdot (mp,l)) ll


(*S Functions upon ML modules. *)

(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a 
   [ml_structure]. *) 

let struct_iter do_decl do_spec s = 
  let rec mt_iter = function 
    | MTident _ -> () 
    | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
    | MTsig (_, sign) -> List.iter spec_iter sign
  and spec_iter = function 
    | (_,Spec s) -> do_spec s
    | (_,Smodule mt) -> mt_iter mt
    | (_,Smodtype mt) -> mt_iter mt
  in
  let rec se_iter = function 
    | (_,SEdecl d) -> do_decl d
    | (_,SEmodule m) -> 
	me_iter m.ml_mod_expr; mt_iter m.ml_mod_type
    | (_,SEmodtype m) -> mt_iter m
  and me_iter = function 
    | MEident _ -> () 
    | MEfunctor (_,mt,me) -> me_iter me; mt_iter mt
    | MEapply (me,me') -> me_iter me; me_iter me'
    | MEstruct (msid, sel) -> List.iter se_iter sel
  in 
  List.iter (function (_,sel) -> List.iter se_iter sel) s

(*s Apply some fonctions upon all references in [ml_type], [ml_ast], 
  [ml_decl], [ml_spec] and [ml_structure]. *)

type do_ref = global_reference -> unit

let record_iter_references do_term = function 
  | Record l -> List.iter do_term l 
  | _ -> ()

let type_iter_references do_type t = 
  let rec iter = function 
    | Tglob (r,l) -> do_type r; List.iter iter l 
    | Tarr (a,b) -> iter a; iter b 
    | _ -> () 
  in iter t

let ast_iter_references do_term do_cons do_type a = 
  let rec iter a = 
    ast_iter iter a;
    match a with 
      | MLglob r -> do_term r
      | MLcons (i,r,_) -> 
	  if lang () = Ocaml then record_iter_references do_term i; 
	  do_cons r 
      | MLcase (i,_,v) -> 
	  if lang () = Ocaml then record_iter_references do_term i; 
	  Array.iter (fun (r,_,_) -> do_cons r) v
      | _ -> ()
  in iter a

let ind_iter_references do_term do_cons do_type kn ind = 
  let type_iter = type_iter_references do_type in
  let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in 
  let packet_iter ip p = 
    do_type (IndRef ip); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types 
  in
  if lang () = Ocaml then record_iter_references do_term ind.ind_info; 
  Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
  
let decl_iter_references do_term do_cons do_type = 
  let type_iter = type_iter_references do_type 
  and ast_iter = ast_iter_references do_term do_cons do_type in
  function 
    | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind 
    | Dtype (r,_,t) -> do_type r; type_iter t 
    | Dterm (r,a,t) -> do_term r; ast_iter a; type_iter t
    | Dfix(rv,c,t) -> 	
	Array.iter do_term rv; Array.iter ast_iter c; Array.iter type_iter t

let spec_iter_references do_term do_cons do_type = function 
  | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind
  | Stype (r,_,ot) -> do_type r; option_iter (type_iter_references do_type) ot
  | Sval (r,t) -> do_term r; type_iter_references do_type t

let struct_iter_references do_term do_cons do_type = 
  struct_iter 
    (decl_iter_references do_term do_cons do_type) 
    (spec_iter_references do_term do_cons do_type) 

(*s Get all references used in one [ml_structure], either in [list] or [set]. *)

type 'a updown = { mutable up : 'a ; mutable down : 'a }

let struct_get_references empty add struc = 
  let o = { up = empty ; down = empty } in 
  let do_term r = o.down <- add r o.down in
  let do_cons r = o.up <- add r o.up in 
  let do_type = if lang () = Haskell then do_cons else do_term in 
  struct_iter_references do_term do_cons do_type struc; o

let struct_get_references_set = struct_get_references Refset.empty Refset.add

module Orefset = struct 
  type t = { set : Refset.t ; list : global_reference list }
  let empty = { set = Refset.empty ; list = [] }
  let add r o = 
    if Refset.mem r o.set then o 
    else { set = Refset.add r o.set ; list = r :: o.list }
  let set o = o.set
  let list o = o.list
end

let struct_get_references_list struc = 
  let o = struct_get_references Orefset.empty Orefset.add struc in 
  { up = Orefset.list o.up; down = Orefset.list o.down }


(*s Searching occurrences of a particular term (no lifting done). *)

exception Found

let rec ast_search t a = 
  if t a then raise Found else ast_iter (ast_search t) a

let decl_ast_search t = function 
  | Dterm (_,a,_) -> ast_search t a
  | Dfix (_,c,_) -> Array.iter (ast_search t) c
  | _ -> () 

let struct_ast_search t s = 
  try struct_iter (decl_ast_search t) (fun _ -> ()) s; false
  with Found -> true

let rec type_search t = function  
  | Tarr (a,b) -> type_search t a; type_search t b 
  | Tglob (r,l) -> List.iter (type_search t) l
  | u -> if t = u then raise Found

let decl_type_search t = function 
  | Dind (_,{ind_packets=p})  -> 
      Array.iter 
	(fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p
  | Dterm (_,_,u) -> type_search t u
  | Dfix (_,_,v) -> Array.iter (type_search t) v
  | Dtype (_,_,u) -> type_search t u

let spec_type_search t = function 
  | Sind (_,{ind_packets=p}) -> 
      Array.iter 
	(fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p
  | Stype (_,_,ot) -> option_iter (type_search t) ot
  | Sval (_,u) -> type_search t u

let struct_type_search t s = 
  try struct_iter (decl_type_search t) (spec_type_search t) s; false
  with Found -> true


(*s Generating the signature. *)

let rec msig_of_ms = function 
  | [] -> [] 
  | (l,SEdecl (Dind (kn,i))) :: ms -> 
      (l,Spec (Sind (kn,i))) :: (msig_of_ms ms)
  | (l,SEdecl (Dterm (r,_,t))) :: ms -> 
      (l,Spec (Sval (r,t))) :: (msig_of_ms ms)
  | (l,SEdecl (Dtype (r,v,t))) :: ms -> 
      (l,Spec (Stype (r,v,Some t))) :: (msig_of_ms ms) 
  | (l,SEdecl (Dfix (rv,_,tv))) :: ms -> 
      let msig = ref (msig_of_ms ms) in 
      for i = Array.length rv - 1 downto 0 do 
	msig := (l,Spec (Sval (rv.(i),tv.(i))))::!msig
      done; 
      !msig
  | (l,SEmodule m) :: ms -> (l,Smodule m.ml_mod_type) :: (msig_of_ms ms)
  | (l,SEmodtype m) :: ms -> (l,Smodtype m) :: (msig_of_ms ms)

let signature_of_structure s = 
  List.map (fun (mp,ms) -> mp,msig_of_ms ms) s 


(*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *)

let get_decl_in_structure r struc = 
  try 
    let base_mp,ll = labels_of_ref r in 
    if not (at_toplevel base_mp) then error_not_visible r;
    let sel = List.assoc base_mp struc in
    let rec go ll sel = match ll with 
      | [] -> assert false
      | l :: ll -> 
	  match List.assoc l sel with 
	    | SEdecl d -> d 
	    | SEmodtype m -> assert false
	    | SEmodule m ->
		match m.ml_mod_expr with 
		  | MEstruct (_,sel) -> go ll sel 
		  | _ -> error_not_visible r 
    in go ll sel
  with Not_found -> assert false


(*s Optimization of a [ml_structure]. *)

(* Some transformations of ML terms. [optimize_struct] simplify
   all beta redexes (when the argument does not occur, it is just
   thrown away; when it occurs exactly once it is substituted; otherwise
   a let-in redex is created for clarity) and iota redexes, plus some other
   optimizations. *)

let dfix_to_mlfix rv av i = 
  let rec make_subst n s = 
    if n < 0 then s 
    else make_subst (n-1) (Refmap.add rv.(n) (n+1) s)
  in 
  let s = make_subst (Array.length rv - 1) Refmap.empty 
  in 
  let rec subst n t = match t with 
    | MLglob ((ConstRef kn) as refe) -> 
	(try MLrel (n + (Refmap.find refe s)) with Not_found -> t)
    | _ -> ast_map_lift subst n t 
  in 
  let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in 
  let c = Array.map (subst 0) av 
  in MLfix(i, ids, c)

let rec optim prm s = function
  | [] -> []
  | (Dtype (r,_,Tdummy) | Dterm(r,MLdummy,_)) as d :: l ->
      if List.mem r prm.to_appear then d :: (optim prm s l) else optim prm s l
  | Dterm (r,t,typ) :: l ->
      let t = normalize (ast_glob_subst !s t) in 
      let i = inline r t in 
      if i then s := Refmap.add r t !s; 
      if not i || prm.modular || List.mem r prm.to_appear 
      then 
	let d = match optimize_fix t with 
	  | MLfix (0, _, [|c|]) -> 
	      Dfix ([|r|], [|ast_subst (MLglob r) c|], [|typ|])
	  | t -> Dterm (r, t, typ)
	in d :: (optim prm s l)
      else optim prm s l
  | d :: l -> d :: (optim prm s l)

let rec optim_se top prm s = function 
  | [] -> [] 
  | (l,SEdecl (Dterm (r,a,t))) :: lse -> 
      let a = normalize (ast_glob_subst !s a) in 
      let i = inline r a in 
      if i then s := Refmap.add r a !s; 
      if top && i && not prm.modular && not (List.mem r prm.to_appear)
      then optim_se top prm s lse
      else 
	let d = match optimize_fix a with 
	  | MLfix (0, _, [|c|]) -> 
	      Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
	  | a -> Dterm (r, a, t)
	in (l,SEdecl d) :: (optim_se top prm s lse)
  | (l,SEdecl (Dfix (rv,av,tv))) :: lse -> 
      let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in 
      let all = ref true in 
      (* This fake body ensures that no fixpoint will be auto-inlined. *)
      let fake_body = MLfix (0,[||],[||]) in 
      for i = 0 to Array.length rv - 1 do 
	if inline rv.(i) fake_body
	then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s
	else all := false
      done; 
      if !all && top && not prm.modular 
	&& (array_for_all (fun r -> not (List.mem r prm.to_appear)) rv)  
      then optim_se top prm s lse
      else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top prm s lse)
  | (l,SEmodule m) :: lse -> 
      let m = { m with ml_mod_expr = optim_me prm s m.ml_mod_expr}
      in (l,SEmodule m) :: (optim_se top prm s lse)
  | se :: lse -> se :: (optim_se top prm s lse) 

and optim_me prm s = function 
  | MEstruct (msid, lse) -> MEstruct (msid, optim_se false prm s lse)
  | MEident mp as me -> me
  | MEapply (me, me') -> MEapply (optim_me prm s me, optim_me prm s me')
  | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me prm s me)

let optimize_struct prm before struc = 
  let subst = ref (Refmap.empty : ml_ast Refmap.t) in 
  option_iter (fun l -> ignore (optim prm subst l)) before; 
  List.map (fun (mp,lse) -> (mp, optim_se true prm subst lse)) struc