From 60d0b86575890a4d3c8ade626fba17e7e0883e15 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 5 Jul 2010 10:09:22 +0000 Subject: Extraction: (yet another) rework of the renaming code - Add module parameters in the structure of visible_layer, in order for module params to be part of name clash detection, avoiding this way a source of potentially wrong code. - In case of clash, module params are alpha-renamed to something unique (Foo__XXX where XXX is the number contained in the mbid). This solves some situations that were unsupported by extraction. for instance the "Module F (X:T). Module X:=X. ... End F." - We now check in Coq identifiers the presence of the extraction-reserved string __. If it is found, we issue a warning (which might become an error someday). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13240 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/extraction/common.ml | 237 +++++++++++++++++++++++++------------- plugins/extraction/common.mli | 4 +- plugins/extraction/extract_env.ml | 2 +- plugins/extraction/haskell.ml | 2 +- plugins/extraction/ocaml.ml | 46 ++++---- plugins/extraction/scheme.ml | 2 +- plugins/extraction/table.ml | 24 ++-- plugins/extraction/table.mli | 4 +- 8 files changed, 194 insertions(+), 127 deletions(-) (limited to 'plugins') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 0941ed50f..41ce4d2d4 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -20,7 +20,14 @@ open Mlutil open Modutil open Mod_subst -let string_of_id id = ascii_of_ident (Names.string_of_id id) +let string_of_id id = + let s = Names.string_of_id id in + for i = 0 to String.length s - 2 do + if s.[i] = '_' && s.[i+1] = '_' then warning_id s + done; + ascii_of_ident s + +let is_mp_bound = function MPbound _ -> true | _ -> false (*s Some pretty-print utility functions. *) @@ -62,17 +69,14 @@ let unquote s = for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done; s -let rec dottify = function +let rec qualify delim = function | [] -> assert false | [s] -> s - | s::[""] -> s - | s::l -> (dottify l)^"."^s + | ""::l -> qualify delim l + | s::l -> s^delim^(qualify delim l) -let rec pseudo_qualify up = function - | [] -> assert false - | [s] -> s - | s::[""] -> s - | s::l -> (if up then "" else "_")^(pseudo_qualify true l)^"__"^s +let dottify = qualify "." +let pseudo_qualify = qualify "__" (*s Uppercase/lowercase renamings. *) @@ -183,23 +187,34 @@ let mpfiles_add, mpfiles_mem, mpfiles_list, mpfiles_clear = register_cleanup clear; (add,mem,list,clear) +(*s List of module parameters that we should alpha-rename *) + +let params_ren_add, params_ren_mem = + let m = ref MPset.empty in + let add mp = m:=MPset.add mp !m + and mem mp = MPset.mem mp !m + and clear () = m:=MPset.empty + in + register_cleanup clear; + (add,mem) + (*s table indicating the visible horizon at a precise moment, i.e. the stack of structures we are inside. - The sequence of [mp] parts should have the following form: - [X.Y; X; A.B.C; A.B; A; ...], i.e. each addition should either - be a [MPdot] over the last entry, or something new, mainly - [MPself], or [MPfile] at the beginning. + a [MPfile] at the beginning, and then more and more [MPdot] + over this [MPfile]. - - The [content] part is used to recoard all the names already - seen at this level. + - the [params] are the [MPbound] when [mp] is a functor, + the innermost [MPbound] coming first in the list. - - The [subst] part is here mainly for printing signature - (in which names are still short, i.e. relative to a [msid]). + - The [content] part is used to record all the names already + seen at this level. *) type visible_layer = { mp : module_path; - content : ((kind*string),unit) Hashtbl.t } + params : module_path list; + content : ((kind*string),label) Hashtbl.t } let pop_visible, push_visible, get_visible = let vis = ref [] in @@ -210,15 +225,15 @@ let pop_visible, push_visible, get_visible = if get_phase () = Impl && modular () && is_modfile v.mp then add_mpfiles_content v.mp v.content; vis := List.tl !vis - and push mp = - vis := { mp = mp; content = Hashtbl.create 97 } :: !vis + and push mp mps = + vis := { mp = mp; params = mps; content = Hashtbl.create 97 } :: !vis and get () = !vis in (pop,push,get) let get_visible_mps () = List.map (function v -> v.mp) (get_visible ()) let top_visible () = match get_visible () with [] -> assert false | v::_ -> v let top_visible_mp () = (top_visible ()).mp -let add_visible ks = Hashtbl.add (top_visible ()).content ks () +let add_visible ks l = Hashtbl.add (top_visible ()).content ks l (* table of local module wrappers used to provide non-ambiguous names *) @@ -284,7 +299,10 @@ let rec mp_renaming_fun mp = match mp with let lmp = mp_renaming mp in if lmp = [""] then (modfstlev_rename l)::lmp else (modular_rename Mod (id_of_label l))::lmp - | MPbound mbid -> [modular_rename Mod (id_of_mbid mbid)] + | MPbound mbid -> + let s = modular_rename Mod (id_of_mbid mbid) in + if not (params_ren_mem mp) then [s] + else let i,_,_ = repr_mbid mbid in [s^"__"^string_of_int i] | MPfile _ when not (modular ()) -> assert false (* see [at_toplevel] above *) | MPfile _ -> assert (get_phase () = Pre); @@ -296,7 +314,9 @@ let rec mp_renaming_fun mp = match mp with and mp_renaming = let add,get,_ = mktable true in - fun x -> try get x with Not_found -> let y = mp_renaming_fun x in add x y; y + fun x -> + try if is_mp_bound (base_mp x) then raise Not_found; get x + with Not_found -> let y = mp_renaming_fun x in add x y; y (*s Renamings creation for a [global_reference]: we build its fully-qualified name in a [string list] form (head is the short name). *) @@ -320,7 +340,9 @@ let ref_renaming_fun (k,r) = let ref_renaming = let add,get,_ = mktable true in - fun x -> try get x with Not_found -> let y = ref_renaming_fun x in add x y; y + fun x -> + try if is_mp_bound (base_mp (modpath_of_r (snd x))) then raise Not_found; get x + with Not_found -> let y = ref_renaming_fun x in add x y; y (* [visible_clash mp0 (k,s)] checks if [mp0-s] of kind [k] can be printed as [s] in the current context of visible @@ -338,12 +360,38 @@ let mpfiles_clash mp0 ks = clash (fun mp -> Hashtbl.mem (get_mpfiles_content mp)) mp0 ks (List.rev (mpfiles_list ())) +let rec params_lookup mp0 ks = function + | [] -> false + | param :: _ when mp0 = param -> true + | param :: params -> + if ks = (Mod, List.hd (mp_renaming param)) then params_ren_add param; + params_lookup mp0 ks params + let visible_clash mp0 ks = let rec clash = function | [] -> false | v :: _ when v.mp = mp0 -> false - | v :: _ when Hashtbl.mem v.content ks -> true - | _ :: vis -> clash vis + | v :: vis -> + let b = Hashtbl.mem v.content ks in + if b && not (is_mp_bound mp0) then true + else begin + if b then params_ren_add mp0; + if params_lookup mp0 ks v.params then false + else clash vis + end + in clash (get_visible ()) + +(* Same, but with verbose output (and mp0 shouldn't be a MPbound) *) + +let visible_clash_dbg mp0 ks = + let rec clash = function + | [] -> None + | v :: _ when v.mp = mp0 -> None + | v :: vis -> + try Some (v.mp,Hashtbl.find v.content ks) + with Not_found -> + if params_lookup mp0 ks v.params then None + else clash vis in clash (get_visible ()) (* After the 1st pass, we can decide which modules will be opened initially *) @@ -370,81 +418,106 @@ let opened_libraries () = (* First, a function that factorize the printing of both [global_reference] and module names for ocaml. When [k=Mod] then [olab=None], otherwise it contains the label of the reference to print. - Invariant: [List.length ls >= 2], simpler situations are handled elsewhere. *) - -let pp_ocaml_gen k mp ls olab = - try (* what is the largest prefix of [mp] that belongs to [visible]? *) - let prefix = common_prefix_from_list mp (get_visible_mps ()) in - let delta = mp_length mp - mp_length prefix in - assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *) - let ls = list_firstn (delta + if k = Mod then 0 else 1) ls in - let s,ls' = list_sep_last ls in - (* Reference r / module path mp is of the form [.s.]. - Difficulty: in ocaml the prefix part cannot be used for - qualification (we are inside it) and the rest of the long - name may be hidden. - Solution: we duplicate the _definition_ of r / mp in a Coq__XXX module *) - let k' = if ls' = [] then k else Mod in - if visible_clash prefix (k',s) then - let front = if ls' = [] && k <> Mod then [s] else ls' in - let lab = (* label associated with s *) - if delta = 0 && k <> Mod then Option.get olab - else get_nth_label_mp delta mp - in - try dottify (front @ [check_duplicate prefix lab]) - with Not_found -> - assert (get_phase () = Pre); (* otherwise it's too late *) - add_duplicate prefix lab; dottify ls - else dottify ls - with Not_found -> - (* [mp] belongs to a closed module, not one of [visible]. *) - let base = base_mp mp in - let base_s,ls1 = list_sep_last ls in - let s,ls2 = list_sep_last ls1 in - (* [List.rev ls] is [base_s :: s :: List.rev ls2] *) - let k' = if ls2 = [] then k else Mod in - if modular () && (mpfiles_mem base) && - (not (mpfiles_clash base (k',s))) && - (not (visible_clash base (k',s))) - then (* Standard situation of an object in another file: *) - (* Thanks to the "open" of this file we remove its name *) - dottify ls1 - else if visible_clash base (Mod,base_s) then - error_module_clash base_s - else dottify ls - -let pp_haskell_gen k mp ls = - if not (modular ()) then List.hd ls - else match List.rev ls with + [rls] is the string list giving the qualified name, short name at the end. + Invariant: [List.length rls >= 2], simpler situations are handled elsewhere. *) + +(* [pp_ocaml_bound] : [mp] starts with a [MPbound] *) + +let pp_ocaml_bound k base mp rls olab = + (* clash with a MPbound will be detected and fixed by renaming this MPbound *) + if get_phase () = Pre then ignore (visible_clash base (Mod,List.hd rls)); + dottify rls + +(* [pp_ocaml_local] : [mp] has something in common with [top_visible ()] + but isn't equal to it *) + +let pp_ocaml_local k _ mp rls olab = + (* what is the largest prefix of [mp] that belongs to [visible]? *) + let prefix = common_prefix_from_list mp (get_visible_mps ()) in + assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *) + let rls = list_skipn (mp_length prefix) rls in + let k',s,rls' = match rls with | [] -> assert false - | s::ls' -> - (if base_mp mp <> top_visible_mp () then s ^ "." else "") ^ - (pseudo_qualify (upperkind k) (List.rev ls')) + | [s] -> k,s,[] + | s::rls' -> Mod,s,rls' + in + (* Reference r / module path mp is of the form [.s.]. + Difficulty: in ocaml the prefix part cannot be used for + qualification (we are inside it) and the rest of the long + name may be hidden. + Solution: we duplicate the _definition_ of r / mp in a Coq__XXX module *) + if not (visible_clash prefix (k',s)) then dottify rls + else + let front = if rls' = [] && k <> Mod then [s] else rls' in + let lab = (* label associated with s *) + if prefix = mp then Option.get olab (* here k<>Mod, see assert above *) + else get_nth_label_mp (mp_length mp - mp_length prefix) mp + in + try dottify (check_duplicate prefix lab :: front) + with Not_found -> + assert (get_phase () = Pre); (* otherwise it's too late *) + add_duplicate prefix lab; dottify rls + +(* [pp_ocaml_extern] : [mp] isn't local, it is defined in another [MPfile]. *) + +let pp_ocaml_extern k base _ rls _ = + match rls with + | [] | [_] -> assert false + | base_s :: s :: rls' -> + let k' = if rls' = [] then k else Mod in + if modular () && (mpfiles_mem base) && + (not (mpfiles_clash base (k',s))) && + (not (visible_clash base (k',s))) + then (* Standard situation of an object in another file: *) + (* Thanks to the "open" of this file we remove its name *) + dottify (s::rls') + else match visible_clash_dbg base (Mod,base_s) with + | None -> dottify rls + | Some (mp,l) -> error_module_clash base (MPdot (mp,l)) + +let pp_ocaml_gen k mp rls olab = + let base = base_mp mp in + let is_local = (base = base_mp (top_visible_mp ())) in + let pp = match base with + | MPdot _ -> assert false + | MPbound _ -> pp_ocaml_bound + | MPfile _ when is_local -> pp_ocaml_local + | MPfile _ -> pp_ocaml_extern + in pp k base mp rls olab + +let pp_haskell_gen k mp rls = match rls with + | [] -> assert false + | s::rls' -> + (if base_mp mp <> top_visible_mp () then s ^ "." else "") ^ + (if upperkind k then "" else "_") ^ pseudo_qualify rls' let pp_global k r = let ls = ref_renaming (k,r) in assert (List.length ls > 1); let s = List.hd ls in + let l = label_of_r r in let mp = modpath_of_r r in if mp = top_visible_mp () then (* simpliest situation: definition of r (or use in the same context) *) (* we update the visible environment *) - (add_visible (k,s); unquote s) - else match lang () with - | Scheme -> unquote s (* no modular Scheme extraction... *) - | Haskell -> pp_haskell_gen k mp ls - | Ocaml -> pp_ocaml_gen k mp ls (Some (label_of_r r)) + (add_visible (k,s) l; unquote s) + else + let rls = List.rev ls in (* for what come next it's easier this way *) + match lang () with + | Scheme -> unquote s (* no modular Scheme extraction... *) + | Haskell -> if modular () then pp_haskell_gen k mp rls else s + | Ocaml -> pp_ocaml_gen k mp rls (Some (label_of_r r)) (* The next function is used only in Ocaml extraction...*) let pp_module mp = let ls = mp_renaming mp in if List.length ls = 1 then dottify ls else match mp with - | MPdot (mp0,_) when mp0 = top_visible_mp () -> + | MPdot (mp0,l) when mp0 = top_visible_mp () -> (* simpliest situation: definition of mp (or use in the same context) *) (* we update the visible environment *) let s = List.hd ls in - add_visible (Mod,s); s - | _ -> pp_ocaml_gen Mod mp ls None + add_visible (Mod,s) l; s + | _ -> pp_ocaml_gen Mod mp (List.rev ls) None diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 33c14e33a..b992f0557 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -43,7 +43,9 @@ val pp_global : kind -> global_reference -> string val pp_module : module_path -> string val top_visible_mp : unit -> module_path -val push_visible : module_path -> unit +(* In [push_visible], the [module_path list] corresponds to + module parameters, the innermost one coming first in the list *) +val push_visible : module_path -> module_path list -> unit val pop_visible : unit -> unit val check_duplicate : module_path -> label -> string diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 2fca8016c..3210f2f16 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -366,7 +366,7 @@ let print_one_decl struc mp decl = set_phase Pre; ignore (d.pp_struct struc); set_phase Impl; - push_visible mp; + push_visible mp []; msgnl (d.pp_decl decl); pop_visible () diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index ce9fab735..e03c7313a 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -326,7 +326,7 @@ and pp_module_expr = function let pp_struct = let pp_sel (mp,sel) = - push_visible mp; + push_visible mp []; let p = prlist_strict pp_structure_elem sel in pop_visible (); p in diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 377648422..ceb2246ad 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -607,8 +607,8 @@ let rec pp_specif = function pp_alias_spec ren s with Not_found -> pp_spec s) | (l,Smodule mt) -> - let def = pp_module_type mt in - let def' = pp_module_type mt in + let def = pp_module_type [] mt in + let def' = pp_module_type [] mt in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++ (try @@ -616,7 +616,7 @@ let rec pp_specif = function fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def') with Not_found -> Pp.mt ()) | (l,Smodtype mt) -> - let def = pp_module_type mt in + let def = pp_module_type [] mt in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++ (try @@ -624,16 +624,16 @@ let rec pp_specif = function fnl () ++ str ("module type "^ren^" = ") ++ name with Not_found -> Pp.mt ()) -and pp_module_type = function +and pp_module_type params = function | MTident kn -> pp_modname kn | MTfunsig (mbid, mt, mt') -> - let typ = pp_module_type mt in + let typ = pp_module_type [] mt in let name = pp_modname (MPbound mbid) in - let def = pp_module_type mt' in + let def = pp_module_type (MPbound mbid :: params) mt' in str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def - | MTsig (mp1, sign) -> - push_visible mp1; + | MTsig (mp, sign) -> + push_visible mp params; let l = map_succeed pp_specif sign in pop_visible (); str "sig " ++ fnl () ++ @@ -648,9 +648,9 @@ and pp_module_type = function in let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l)) in - push_visible mp_mt; + push_visible mp_mt []; let s = - pp_module_type mt ++ str " with type " ++ + pp_module_type [] mt ++ str " with type " ++ pp_global Type r ++ ids in pop_visible(); @@ -660,9 +660,9 @@ and pp_module_type = function let mp_w = List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl in - push_visible mp_mt; + push_visible mp_mt []; let s = - pp_module_type mt ++ str " with module " ++ pp_modname mp_w + pp_module_type [] mt ++ str " with module " ++ pp_modname mp_w in pop_visible (); s ++ str " = " ++ pp_modname mp @@ -681,10 +681,10 @@ let rec pp_structure_elem = function let typ = (* virtual printing of the type, in order to have a correct mli later*) if Common.get_phase () = Pre then - str ": " ++ pp_module_type m.ml_mod_type + str ": " ++ pp_module_type [] m.ml_mod_type else mt () in - let def = pp_module_expr m.ml_mod_expr in + let def = pp_module_expr [] m.ml_mod_expr in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 (str "module " ++ name ++ typ ++ str " = " ++ @@ -694,7 +694,7 @@ let rec pp_structure_elem = function fnl () ++ str ("module "^ren^" = ") ++ name with Not_found -> mt ()) | (l,SEmodtype m) -> - let def = pp_module_type m in + let def = pp_module_type [] m in let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++ (try @@ -702,17 +702,17 @@ let rec pp_structure_elem = function fnl () ++ str ("module type "^ren^" = ") ++ name with Not_found -> mt ()) -and pp_module_expr = function - | MEident mp' -> pp_modname mp' +and pp_module_expr params = function + | MEident mp -> pp_modname mp + | MEapply (me, me') -> + pp_module_expr [] me ++ str "(" ++ pp_module_expr [] me' ++ str ")" | MEfunctor (mbid, mt, me) -> let name = pp_modname (MPbound mbid) in - let typ = pp_module_type mt in - let def = pp_module_expr me in + let typ = pp_module_type [] mt in + let def = pp_module_expr (MPbound mbid :: params) me in str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def - | MEapply (me, me') -> - pp_module_expr me ++ str "(" ++ pp_module_expr me' ++ str ")" | MEstruct (mp, sel) -> - push_visible mp; + push_visible mp params; let l = map_succeed pp_structure_elem sel in pop_visible (); str "struct " ++ fnl () ++ @@ -723,7 +723,7 @@ let do_struct f s = let pp s = try f s ++ fnl2 () with Failure "empty phrase" -> mt () in let ppl (mp,sel) = - push_visible mp; + push_visible mp []; let p = prlist_strict pp sel in (* for monolithic extraction, we try to simulate the unavailability of [MPfile] in names by artificially nesting these [MPfile] *) diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 9c600760f..64b86e6e2 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -195,7 +195,7 @@ and pp_module_expr = function let pp_struct = let pp_sel (mp,sel) = - push_visible mp; + push_visible mp []; let p = prlist_strict pp_structure_elem sel in pop_visible (); p in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index a380654c6..6691e2622 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -82,7 +82,7 @@ let rec get_nth_label_mp n = function let common_prefix_from_list mp0 mpl = let prefixes = prefixes_mp mp0 in let rec f = function - | [] -> raise Not_found + | [] -> assert false | mp :: l -> if MPset.mem mp prefixes then mp else f l in f mpl @@ -108,19 +108,6 @@ let labels_of_ref r = in parse_labels2 [l] mp_top mp - - - -let labels_of_ref2 r = - let mp1,_,l = - match r with - ConstRef con -> repr_con con - | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> repr_mind kn - | VarRef _ -> assert false - in mp1,l - - let rec add_labels_mp mp = function | [] -> mp | l :: ll -> add_labels_mp (MPdot (mp,l)) ll @@ -287,6 +274,10 @@ let check_inside_section () = err (str "You can't do that within a section." ++ fnl () ++ str "Close it and try again.") +let warning_id s = + msg_warning (str ("The identifier "^s^ + " contains __ which is reserved for the extraction")) + let error_constant r = err (safe_pr_global r ++ str " is not a constant.") @@ -296,8 +287,9 @@ let error_inductive r = let error_nb_cons () = err (str "Not the right number of constructors.") -let error_module_clash s = - err (str ("There are two Coq modules with ML name " ^ s ^".\n") ++ +let error_module_clash mp1 mp2 = + err (str "The Coq modules " ++ pr_long_mp mp1 ++ str " and " ++ + pr_long_mp mp2 ++ str " have the same ML name.\n" ++ str "This is not supported yet. Please do some renaming first.") let error_unknown_module m = diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index b215e373e..e64f1de15 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -18,11 +18,12 @@ val safe_basename_of_global : global_reference -> identifier val warning_axioms : unit -> unit val warning_both_mod_and_cst : qualid -> module_path -> global_reference -> unit +val warning_id : string -> unit val error_axiom_scheme : global_reference -> int -> 'a val error_constant : global_reference -> 'a val error_inductive : global_reference -> 'a val error_nb_cons : unit -> 'a -val error_module_clash : string -> 'a +val error_module_clash : module_path -> module_path -> 'a val error_unknown_module : qualid -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a @@ -56,7 +57,6 @@ val common_prefix_from_list : module_path -> module_path list -> module_path val add_labels_mp : module_path -> label list -> module_path val get_nth_label_mp : int -> module_path -> label val labels_of_ref : global_reference -> module_path * label list -val labels_of_ref2 : global_reference -> module_path * label (*s Some table-related operations *) -- cgit v1.2.3