diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/common.ml | 8 | ||||
| -rw-r--r-- | plugins/extraction/common.mli | 2 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/miniml.mli | 4 | ||||
| -rw-r--r-- | plugins/extraction/mlutil.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/modutil.ml | 8 | ||||
| -rw-r--r-- | plugins/extraction/ocaml.ml | 6 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 8 | ||||
| -rw-r--r-- | plugins/extraction/table.mli | 8 |
10 files changed, 25 insertions, 25 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index bd5e2291ac..d8e489be74 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -255,7 +255,7 @@ let params_ren_add, params_ren_mem = type visible_layer = { mp : module_path; params : module_path list; - content : ((kind*string),label) Hashtbl.t } + content : ((kind*string),Label.t) Hashtbl.t } let pop_visible, push_visible, get_visible = let vis = ref [] in @@ -321,7 +321,7 @@ let modfstlev_rename = let add_prefixes,get_prefixes,_ = mktable true in fun l -> let coqid = Id.of_string "Coq" in - let id = id_of_label l in + let id = Label.to_id l in try let coqset = get_prefixes id in let nextcoq = next_ident_away coqid coqset in @@ -341,7 +341,7 @@ let rec mp_renaming_fun mp = match mp with | MPdot (mp,l) -> let lmp = mp_renaming mp in if lmp = [""] then (modfstlev_rename l)::lmp - else (modular_rename Mod (id_of_label l))::lmp + else (modular_rename Mod (Label.to_id l))::lmp | MPbound mbid -> let s = modular_rename Mod (id_of_mbid mbid) in if not (params_ren_mem mp) then [s] @@ -584,7 +584,7 @@ let pp_module mp = the constants are directly turned into chars *) let mk_ind path s = - make_mind (MPfile (dirpath_of_string path)) Dir_path.empty (mk_label s) + make_mind (MPfile (dirpath_of_string path)) Dir_path.empty (Label.make s) let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii" diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 9ddd0f2aff..0fd3e7bb7b 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -63,7 +63,7 @@ val top_visible_mp : unit -> module_path val push_visible : module_path -> module_path list -> unit val pop_visible : unit -> unit -val check_duplicate : module_path -> label -> string +val check_duplicate : module_path -> Label.t -> string type reset_kind = AllButExternal | Everything diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 7540167158..7f5ad4f660 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -208,7 +208,7 @@ let env_for_mtb_with_def env mp seb idl = | SEBstruct(sig_b) -> sig_b | _ -> assert false in - let l = label_of_id (List.hd idl) in + let l = Label.of_id (List.hd idl) in let spot = function (l',SFBconst _) -> l = l' | _ -> false in let before = fst (List.split_when spot sig_b) in Modops.add_signature mp before empty_delta_resolver env diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index b892ae57a5..5ab3647d67 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -450,7 +450,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) | Anonymous::l, typ::typs -> None :: (select_fields l typs) | Name id::l, typ::typs -> - let knp = make_con mp d (label_of_id id) in + let knp = make_con mp d (Label.of_id id) in (* Is it safe to use [id] for projections [foo.id] ? *) if List.for_all ((=) Keep) (type2signature env typ) then projs := Cset.add knp !projs; diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 14a30ae796..104a4c8657 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -157,7 +157,7 @@ and ml_with_declaration = | ML_With_type of Id.t list * Id.t list * ml_type | ML_With_module of Id.t list * module_path -and ml_module_sig = (label * ml_specif) list +and ml_module_sig = (Label.t * ml_specif) list type ml_structure_elem = | SEdecl of ml_decl @@ -170,7 +170,7 @@ and ml_module_expr = | MEstruct of module_path * ml_module_structure | MEapply of ml_module_expr * ml_module_expr -and ml_module_structure = (label * ml_structure_elem) list +and ml_module_structure = (Label.t * ml_structure_elem) list and ml_module = { ml_mod_expr : ml_module_expr; diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index bcdee5954d..dba77b923a 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1306,7 +1306,7 @@ let inline_test r t = let con_of_string s = let null = Dir_path.empty in match Dir_path.repr (dirpath_of_string s) with - | id :: d -> make_con (MPfile (Dir_path.make d)) null (label_of_id id) + | id :: d -> make_con (MPfile (Dir_path.make d)) null (Label.of_id id) | [] -> assert false let manual_inline_set = diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 9746c39e49..0ed6a28558 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -32,14 +32,14 @@ let se_iter do_decl do_spec do_mp = let mp_mt = msid_of_mt mt in let l',idl' = List.sep_last idl in let mp_w = - List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl' + List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in - let r = ConstRef (make_con mp_w Dir_path.empty (label_of_id l')) in + let r = ConstRef (make_con mp_w Dir_path.empty (Label.of_id l')) in mt_iter mt; do_decl (Dtype(r,l,t)) | MTwith (mt,ML_With_module(idl,mp))-> let mp_mt = msid_of_mt mt in let mp_w = - List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl + List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl in mt_iter mt; do_mp mp_w; do_mp mp | MTsig (_, sign) -> List.iter spec_iter sign @@ -249,7 +249,7 @@ let dfix_to_mlfix rv av i = (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 ids = Array.map (fun r -> Label.to_id (label_of_r r)) rv in let c = Array.map (subst 0) av in MLfix(i, ids, c) diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 7742dd7834..fbd3fd4ea8 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -648,9 +648,9 @@ and pp_module_type params = function let mp_mt = msid_of_mt mt in let l,idl' = List.sep_last idl in let mp_w = - List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl' + List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in - let r = ConstRef (make_con mp_w Dir_path.empty (label_of_id l)) in + let r = ConstRef (make_con mp_w Dir_path.empty (Label.of_id l)) in push_visible mp_mt []; let pp_w = str " with type " ++ ids ++ pp_global Type r in pop_visible(); @@ -658,7 +658,7 @@ and pp_module_type params = function | MTwith(mt,ML_With_module(idl,mp)) -> let mp_mt = msid_of_mt mt in let mp_w = - List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl + List.fold_left (fun mp id -> MPdot(mp,Label.of_id id)) mp_mt idl in push_visible mp_mt []; let pp_w = str " with module " ++ pp_modname mp_w in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index a541211391..74728f4124 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -175,7 +175,7 @@ let add_recursors env kn = make_con_equiv (modpath (user_mind kn)) (modpath (canonical_mind kn)) - Dir_path.empty (label_of_id id) + Dir_path.empty (Label.of_id id) in let mib = Environ.lookup_mind kn env in Array.iter @@ -245,8 +245,8 @@ let safe_basename_of_global r = anomaly "Inductive object unknown to extraction and not globally visible" in match r with - | ConstRef kn -> id_of_label (con_label kn) - | IndRef (kn,0) -> id_of_label (mind_label kn) + | ConstRef kn -> Label.to_id (con_label kn) + | IndRef (kn,0) -> Label.to_id (mind_label kn) | IndRef (kn,i) -> (try (snd (lookup_ind kn)).ind_packets.(i).ip_typename with Not_found -> last_chance r) @@ -268,7 +268,7 @@ let safe_pr_long_global r = with _ -> match r with | ConstRef kn -> let mp,_,l = repr_con kn in - str ((string_of_mp mp)^"."^(string_of_label l)) + str ((string_of_mp mp)^"."^(Label.to_string l)) | _ -> assert false let pr_long_mp mp = diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 2cf3c475ed..b69715fc93 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -46,9 +46,9 @@ val info_file : string -> unit (*s utilities about [module_path] and [kernel_names] and [global_reference] *) val occur_kn_in_ref : mutual_inductive -> global_reference -> bool -val repr_of_r : global_reference -> module_path * Dir_path.t * label +val repr_of_r : global_reference -> module_path * Dir_path.t * Label.t val modpath_of_r : global_reference -> module_path -val label_of_r : global_reference -> label +val label_of_r : global_reference -> Label.t val current_toplevel : unit -> module_path val base_mp : module_path -> module_path val is_modfile : module_path -> bool @@ -61,8 +61,8 @@ val mp_length : module_path -> int val prefixes_mp : module_path -> MPset.t val common_prefix_from_list : module_path -> module_path list -> module_path option -val get_nth_label_mp : int -> module_path -> label -val labels_of_ref : global_reference -> module_path * label list +val get_nth_label_mp : int -> module_path -> Label.t +val labels_of_ref : global_reference -> module_path * Label.t list (*s Some table-related operations *) |