summaryrefslogtreecommitdiff
path: root/contrib/extraction/modutil.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
committerGravatar Samuel Mimram <samuel.mimram@ens-lyon.org>2004-07-28 21:54:47 +0000
commit6b649aba925b6f7462da07599fe67ebb12a3460e (patch)
tree43656bcaa51164548f3fa14e5b10de5ef1088574 /contrib/extraction/modutil.ml
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'contrib/extraction/modutil.ml')
-rw-r--r--contrib/extraction/modutil.ml405
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