1 files changed, 405 insertions, 0 deletions
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
new file mode 100644
index 00000000..feb9e54e
--- /dev/null
+++ b/contrib/extraction/modutil.ml
@@ -0,0 +1,405 @@
+(************************************************************************)
+(*  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,v 1.7.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+
+open Names
+open Declarations
+open Environ
+open Libnames
+open Util
+open Miniml
+open Table
+open Mlutil
+
+(*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 
+    match elem with 
+      | SEBconst cb -> Environ.add_constant kn 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_kn kn = 
+  let mp,_,l = repr_kn kn 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 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 (r,_) -> do_cons r
+      | MLcase (_,v) as a -> 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 ind.ind_info = Record then List.iter do_term (find_projections kn); 
+  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 kn = kn_of_r r in 
+    let base_mp,ll = labels_of_kn kn 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) (KNmap.add (kn_of_r rv.(n)) (n+1) s)
+  in 
+  let s = make_subst (Array.length rv - 1) KNmap.empty 
+  in 
+  let rec subst n t = match t with 
+    | MLglob (ConstRef kn) -> 
+	(try MLrel (n + (KNmap.find kn s)) with Not_found -> t)
+    | _ -> ast_map_lift subst n t 
+  in 
+  let ids = Array.map (fun r -> id_of_label (label (kn_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 := KNmap.add (kn_of_r 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 kn = kn_of_r r in 
+      let a = normalize (ast_glob_subst !s a) in 
+      let i = inline r a in 
+      if i then s := KNmap.add kn 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 := KNmap.add (kn_of_r 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 (KNmap.empty : ml_ast KNmap.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