diff options
Diffstat (limited to 'plugins')
27 files changed, 175 insertions, 152 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index e1edeec37e..47381f6d80 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -203,7 +203,7 @@ let pop_visible, push_visible, get_visible, subst_mp = and push mp o = vis := { mp = mp; content = Hashtbl.create 97 } :: !vis; let s = List.hd !sub in - let s = match o with None -> s | Some msid -> add_msid msid mp s in + let s = match o with None -> s | Some msid -> add_mp msid mp empty_delta_resolver s in sub := s :: !sub and get () = !vis and subst mp = subst_mp (List.hd !sub) mp @@ -278,7 +278,6 @@ 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 - | MPself msid -> [modular_rename Mod (id_of_msid msid)] | MPbound mbid -> [modular_rename Mod (id_of_mbid mbid)] | MPfile _ when not (modular ()) -> assert false (* see [at_toplevel] above *) | MPfile _ -> diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index c401bd0592..a68e72d261 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -45,7 +45,7 @@ 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 -> mod_self_id option -> unit +val push_visible : module_path -> module_path option -> 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 ba4786d37d..37721c9b96 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -32,7 +32,7 @@ let toplevel_env () = let mp,_,l = repr_kn kn in let seb = match Libobject.object_tag o with | "CONSTANT" -> SFBconst (Global.lookup_constant (constant_of_kn kn)) - | "INDUCTIVE" -> SFBmind (Global.lookup_mind kn) + | "INDUCTIVE" -> SFBmind (Global.lookup_mind (mind_of_kn kn)) | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l))) | "MODULE TYPE" -> SFBmodtype (Global.lookup_modtype (MPdot (mp,l))) @@ -41,8 +41,8 @@ let toplevel_env () = | _ -> failwith "caught" in match current_toplevel () with - | MPself msid -> SEBstruct (msid, List.rev (map_succeed get_reference seg)) - | _ -> assert false + | _ -> SEBstruct (List.rev (map_succeed get_reference seg)) + let environment_until dir_opt = let rec parse = function @@ -69,7 +69,7 @@ module type VISIT = sig (* Add kernel_name / constant / reference / ... in the visit lists. These functions silently add the mp of their arg in the mp list *) - val add_kn : kernel_name -> unit + val add_kn : mutual_inductive -> unit val add_con : constant -> unit val add_ref : global_reference -> unit val add_decl_deps : ml_decl -> unit @@ -77,7 +77,7 @@ module type VISIT = sig (* Test functions: is a particular object a needed dependency for the current extraction ? *) - val needed_kn : kernel_name -> bool + val needed_kn : mutual_inductive -> bool val needed_con : constant -> bool val needed_mp : module_path -> bool end @@ -87,17 +87,17 @@ module Visit : VISIT = struct (for inductives and modules names) and a Cset for constants (and still the remaining MPset) *) type must_visit = - { mutable kn : KNset.t; mutable con : Cset.t; mutable mp : MPset.t } + { mutable kn : Mindset.t; mutable con : Cset.t; mutable mp : MPset.t } (* the imperative internal visit lists *) - let v = { kn = KNset.empty ; con = Cset.empty ; mp = MPset.empty } + let v = { kn = Mindset.empty ; con = Cset.empty ; mp = MPset.empty } (* the accessor functions *) - let reset () = v.kn <- KNset.empty; v.con <- Cset.empty; v.mp <- MPset.empty - let needed_kn kn = KNset.mem kn v.kn + let reset () = v.kn <- Mindset.empty; v.con <- Cset.empty; v.mp <- MPset.empty + let needed_kn kn = Mindset.mem kn v.kn let needed_con c = Cset.mem c v.con let needed_mp mp = MPset.mem mp v.mp let add_mp mp = check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp - let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn) + let add_kn kn = v.kn <- Mindset.add kn v.kn; add_mp (mind_modpath kn) let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c) let add_ref = function | ConstRef c -> add_con c @@ -140,29 +140,29 @@ let factor_fix env l cb msb = labels, recd, msb'' end -let build_mb expr typ_opt = - { mod_expr = Some expr; +let build_mb mp expr typ_opt = + { mod_mp = mp; + mod_expr = Some expr; mod_type = typ_opt; + mod_type_alg = None; mod_constraints = Univ.Constraint.empty; - mod_alias = Mod_subst.empty_subst; + mod_delta = Mod_subst.empty_delta_resolver; mod_retroknowledge = [] } let my_type_of_mb env mb = - match mb.mod_type with - | Some mtb -> mtb - | None -> Modops.eval_struct env (Option.get mb.mod_expr) + mb.mod_type (** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def]. To check with Elie. *) -let env_for_mtb_with env mtb idl = - let msid,sig_b = match Modops.eval_struct env mtb with - | SEBstruct(msid,sig_b) -> msid,sig_b +let env_for_mtb_with env mp mtb idl = + let sig_b = match mtb with + | SEBstruct(sig_b) -> sig_b | _ -> assert false in let l = label_of_id (List.hd idl) in let before = fst (list_split_when (fun (l',_) -> l=l') sig_b) in - Modops.add_signature (MPself msid) before env + Modops.add_signature mp before empty_delta_resolver env (* From a [structure_body] (i.e. a list of [structure_field_body]) to specifications. *) @@ -177,20 +177,18 @@ let rec extract_sfb_spec env mp = function else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmind _) :: msig -> let kn = make_kn mp empty_dirpath l in - let s = Sind (kn, extract_inductive env kn) in + let mind = mind_of_kn kn in + let s = Sind (kn, extract_inductive env mind) in let specs = extract_sfb_spec env mp msig in if logical_spec s then specs else begin Visit.add_spec_deps s; (l,Spec s) :: specs end | (l,SFBmodule mb) :: msig -> let specs = extract_sfb_spec env mp msig in - let spec = extract_seb_spec env (my_type_of_mb env mb) in + let spec = extract_seb_spec env mb.mod_mp (my_type_of_mb env mb) in (l,Smodule spec) :: specs | (l,SFBmodtype mtb) :: msig -> let specs = extract_sfb_spec env mp msig in - (l,Smodtype (extract_seb_spec env mtb.typ_expr)) :: specs - | (l,SFBalias (mp1,typ_opt,_)) :: msig -> - let mb = build_mb (SEBident mp1) typ_opt in - extract_sfb_spec env mp ((l,SFBmodule mb) :: msig) + (l,Smodtype (extract_seb_spec env mtb.typ_mp mtb.typ_expr)) :: specs (* From [struct_expr_body] to specifications *) @@ -201,34 +199,35 @@ let rec extract_sfb_spec env mp = function For instance, [my_type_of_mb] ensures this invariant. *) -and extract_seb_spec env = function +and extract_seb_spec env mp1 = function | SEBident mp -> Visit.add_mp mp; MTident mp | SEBwith(mtb',With_definition_body(idl,cb))-> - let env' = env_for_mtb_with env mtb' idl in - let mtb''= extract_seb_spec env mtb' in + let env' = env_for_mtb_with env mp1 mtb' idl in + let mtb''= extract_seb_spec env mp1 mtb' in (match extract_with_type env' cb with (* cb peut contenir des kn *) | None -> mtb'' | Some (vl,typ) -> MTwith(mtb'',ML_With_type(idl,vl,typ))) - | SEBwith(mtb',With_module_body(idl,mp,_,_))-> + | SEBwith(mtb',With_module_body(idl,mp))-> Visit.add_mp mp; - MTwith(extract_seb_spec env mtb', + MTwith(extract_seb_spec env mp1 mtb', ML_With_module(idl,mp)) (* TODO: On pourrait peut-etre oter certaines eta-expansion, du genre: | SEBfunctor(mbid,_,SEBapply(m,SEBident (MPbound mbid2),_)) when mbid = mbid2 -> extract_seb_spec env m (* faudrait alors ajouter un test de non-apparition de mbid dans mb *) *) - | SEBfunctor (mbid, mtb, mtb') -> + | SEBfunctor (mbid, mtb, mtb') -> let mp = MPbound mbid in - let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in - MTfunsig (mbid, extract_seb_spec env mtb.typ_expr, - extract_seb_spec env' mtb') - | SEBstruct (msid, msig) -> - let mp = MPself msid in - let env' = Modops.add_signature mp msig env in - MTsig (msid, extract_sfb_spec env' mp msig) - | SEBapply _ as mtb -> - extract_seb_spec env (Modops.eval_struct env mtb) + let env' = Modops.add_module (Modops.module_body_of_type mp mtb) + env in + MTfunsig (mbid, extract_seb_spec env mp mtb.typ_expr, + extract_seb_spec env' mp1 mtb') + | SEBstruct (msig) -> + let env' = Modops.add_signature mp1 msig empty_delta_resolver env in + MTsig (mp1, extract_sfb_spec env' mp1 msig) + | SEBapply _ -> + assert false + (* From a [structure_body] (i.e. a list of [structure_field_body]) @@ -263,9 +262,10 @@ let rec extract_sfb env mp all = function | (l,SFBmind mib) :: msb -> let ms = extract_sfb env mp all msb in let kn = make_kn mp empty_dirpath l in - let b = Visit.needed_kn kn in + let mind = mind_of_kn kn in + let b = Visit.needed_kn mind in if all || b then - let d = Dind (kn, extract_inductive env kn) in + let d = Dind (kn, extract_inductive env mind) in if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms @@ -279,40 +279,34 @@ let rec extract_sfb env mp all = function let ms = extract_sfb env mp all msb in let mp = MPdot (mp,l) in if all || Visit.needed_mp mp then - (l,SEmodtype (extract_seb_spec env mtb.typ_expr)) :: ms + (l,SEmodtype (extract_seb_spec env mp mtb.typ_expr)) :: ms else ms - | (l,SFBalias (mp1,typ_opt,_)) :: msb -> - let mb = build_mb (SEBident mp1) typ_opt in - extract_sfb env mp all ((l,SFBmodule mb) :: msb) (* From [struct_expr_body] to implementations *) -and extract_seb env mpo all = function +and extract_seb env mp all = function | SEBident mp -> if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; Visit.add_mp mp; MEident mp | SEBapply (meb, meb',_) -> - MEapply (extract_seb env None true meb, - extract_seb env None true meb') + MEapply (extract_seb env mp true meb, + extract_seb env mp true meb') | SEBfunctor (mbid, mtb, meb) -> - let mp = MPbound mbid in - let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in - MEfunctor (mbid, extract_seb_spec env mtb.typ_expr, - extract_seb env' None true meb) - | SEBstruct (msid, msb) -> - let mp,msb = match mpo with - | None -> MPself msid, msb - | Some mp -> mp, Modops.subst_structure (map_msid msid mp) msb - in - let env' = Modops.add_signature mp msb env in - MEstruct (msid, extract_sfb env' mp all msb) + let mp1 = MPbound mbid in + let env' = Modops.add_module (Modops.module_body_of_type mp1 mtb) + env in + MEfunctor (mbid, extract_seb_spec env mp1 mtb.typ_expr, + extract_seb env' mp true meb) + | SEBstruct (msb) -> + let env' = Modops.add_signature mp msb empty_delta_resolver env in + MEstruct (mp,extract_sfb env' mp all msb) | SEBwith (_,_) -> anomaly "Not available yet" and extract_module env mp all mb = (* [mb.mod_expr <> None ], since we look at modules from outside. *) (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *) - { ml_mod_expr = extract_seb env (Some mp) all (Option.get mb.mod_expr); - ml_mod_type = extract_seb_spec env (my_type_of_mb env mb) } + { ml_mod_expr = extract_seb env mp all (Option.get mb.mod_expr); + ml_mod_type = extract_seb_spec env mp (my_type_of_mb env mb) } let unpack = function MEstruct (_,sel) -> sel | _ -> assert false @@ -324,7 +318,7 @@ let mono_environment refs mpl = let env = Global.env () in let l = List.rev (environment_until None) in List.rev_map - (fun (mp,m) -> mp, unpack (extract_seb env (Some mp) false m)) l + (fun (mp,m) -> mp, unpack (extract_seb env mp false m)) l (**************************************) (*S Part II : Input/Output primitives *) @@ -514,7 +508,7 @@ let extraction_library is_rec m = let l = List.rev (environment_until (Some dir_m)) in let select l (mp,meb) = if Visit.needed_mp mp - then (mp, unpack (extract_seb env (Some mp) true meb)) :: l + then (mp, unpack (extract_seb env mp true meb)) :: l else l in let struc = List.fold_left select [] l in diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 3468e8a360..d119dbe8ec 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -310,7 +310,15 @@ and extract_ind env kn = (* kn is supposed to be in long form *) with Not_found -> (* First, if this inductive is aliased via a Module, *) (* we process the original inductive. *) - Option.iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv; + let equiv = + if (canonical_mind kn) = (user_mind kn) then + NoEquiv + else + begin + ignore (extract_ind env (mind_of_kn (canonical_mind kn))); + Equiv (canonical_mind kn) + end + in (* Everything concerning parameters. *) (* We do that first, since they are common to all the [mib]. *) let mip0 = mib.mind_packets.(0) in @@ -333,13 +341,12 @@ and extract_ind env kn = (* kn is supposed to be in long form *) ip_types = t }) mib.mind_packets in + add_ind kn mib {ind_info = Standard; ind_nparams = npar; ind_packets = packets; - ind_equiv = match mib.mind_equiv with - | None -> NoEquiv - | Some kn -> Equiv kn + ind_equiv = equiv }; (* Second pass: we extract constructors *) for i = 0 to mib.mind_ntypes - 1 do @@ -388,7 +395,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in assert (List.length field_names = List.length typ); let projs = ref Cset.empty in - let mp,d,_ = repr_kn kn in + let mp,d,_ = repr_mind kn in let rec select_fields l typs = match l,typs with | [],[] -> [] | (Name id)::l, typ::typs -> @@ -424,9 +431,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets; - ind_equiv = match mib.mind_equiv with - | None -> NoEquiv - | Some kn -> Equiv kn } + ind_equiv = equiv } in add_ind kn mib i; i diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 2c534ea7b4..6bcd24763f 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -26,7 +26,7 @@ val extract_with_type : env -> constant_body -> ( identifier list * ml_type ) op val extract_fixpoint : env -> constant array -> (constr, types) prec_declaration -> ml_decl -val extract_inductive : env -> kernel_name -> ml_ind +val extract_inductive : env -> mutual_inductive -> ml_ind (*s Is a [ml_decl] or a [ml_spec] logical ? *) diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 9d45c08b7e..6973bb454f 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -84,7 +84,7 @@ let rec pp_type par vl t = | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i)) | Tglob (r,[]) -> pp_global Type r | Tglob (r,l) -> - if r = IndRef (kn_sig,0) then + if r = IndRef (mind_of_kn kn_sig,0) then pp_type true vl (List.hd l) else pp_par par @@ -269,8 +269,8 @@ let pp_string_parameters ids = prlist (fun id -> str id ++ str " ") let pp_decl = function | Dind (kn,i) when i.ind_info = Singleton -> - pp_singleton kn i.ind_packets.(0) ++ fnl () - | Dind (kn,i) -> hov 0 (pp_ind true kn 0 i) + pp_singleton (mind_of_kn kn) i.ind_packets.(0) ++ fnl () + | Dind (kn,i) -> hov 0 (pp_ind true (mind_of_kn kn) 0 i) | Dtype (r, l, t) -> if is_inline_custom r then mt () else diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 55231d766b..91c60d2055 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -128,7 +128,7 @@ type ml_specif = and ml_module_type = | MTident of module_path | MTfunsig of mod_bound_id * ml_module_type * ml_module_type - | MTsig of mod_self_id * ml_module_sig + | MTsig of module_path * ml_module_sig | MTwith of ml_module_type * ml_with_declaration and ml_with_declaration = @@ -145,7 +145,7 @@ type ml_structure_elem = and ml_module_expr = | MEident of module_path | MEfunctor of mod_bound_id * ml_module_type * ml_module_expr - | MEstruct of mod_self_id * ml_module_structure + | MEstruct of module_path * ml_module_structure | MEapply of ml_module_expr * ml_module_expr and ml_module_structure = (label * ml_structure_elem) list diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 213df31e6e..2e9fb8bf28 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -649,9 +649,9 @@ let generalizable_list = let datatypes = MPfile (dirpath_of_string "Coq.Init.Datatypes") and specif = MPfile (dirpath_of_string "Coq.Init.Specif") in - [ make_kn datatypes empty_dirpath (mk_label "bool"); - make_kn specif empty_dirpath (mk_label "sumbool"); - make_kn specif empty_dirpath (mk_label "sumor") ] + [ make_mind datatypes empty_dirpath (mk_label "bool"); + make_mind specif empty_dirpath (mk_label "sumbool"); + make_mind specif empty_dirpath (mk_label "sumor") ] let check_generalizable_case unsafe br = if not unsafe then diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 4b6b47ab95..9c5feac826 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -50,7 +50,7 @@ end (*s Utility functions over ML types without meta *) -val type_mem_kn : kernel_name -> ml_type -> bool +val type_mem_kn : mutual_inductive -> ml_type -> bool val type_maxvar : ml_type -> int diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 1b1a39770d..9195b747e9 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -21,11 +21,7 @@ open Mod_subst (*S Functions upon ML modules. *) let rec msid_of_mt = function - | MTident mp -> begin - match Modops.eval_struct (Global.env()) (SEBident mp) with - | SEBstruct(msid,_) -> MPself msid - | _ -> anomaly "Extraction:the With can't be applied to a funsig" - end + | MTident mp -> mp | MTwith(mt,_)-> msid_of_mt mt | _ -> anomaly "Extraction:the With operator isn't applied to a name" @@ -101,25 +97,26 @@ let ind_iter_references do_term do_cons do_type kn ind = do_type (IndRef ip); if lang () = Ocaml then (match ind.ind_equiv with - | Equiv kne -> do_type (IndRef (kne, snd ip)); + | Miniml.Equiv kne -> do_type (IndRef (mind_of_kn kne, snd 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 + 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 + | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type + (mind_of_kn 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 + | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type (mind_of_kn 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 @@ -190,7 +187,7 @@ let signature_of_structure s = (*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *) let get_decl_in_structure r struc = - try + 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 @@ -311,7 +308,7 @@ let reset_needed, add_needed, found_needed, is_needed = (fun r -> Refset.mem (base_r r) !needed)) let declared_refs = function - | Dind (kn,_) -> [|IndRef (kn,0)|] + | Dind (kn,_) -> [|IndRef (mind_of_kn kn,0)|] | Dtype (r,_,_) -> [|r|] | Dterm (r,_,_) -> [|r|] | Dfix (rv,_,_) -> rv @@ -322,7 +319,7 @@ let declared_refs = function let compute_deps_decl = function | Dind (kn,ind) -> (* Todo Later : avoid dependencies when Extract Inductive *) - ind_iter_references add_needed add_needed add_needed kn ind + ind_iter_references add_needed add_needed add_needed (mind_of_kn kn) ind | Dtype (r,ids,t) -> if not (is_custom r) then type_iter_references add_needed t | Dterm (r,u,t) -> diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 93fc2c2dc4..107b5368f3 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -122,7 +122,7 @@ let find_projections = function Record l -> l | _ -> raise NoRecord let kn_sig = let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in - make_kn specif empty_dirpath (mk_label "sig") + make_mind specif empty_dirpath (mk_label "sig") let rec pp_type par vl t = let rec pp_rec par = function @@ -380,7 +380,7 @@ let pp_Dfix (rv,c,t) = let pp_equiv param_list name = function | NoEquiv, _ -> mt () | Equiv kn, i -> - str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (kn,i)) + str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (mind_of_kn kn,i)) | RenEquiv ren, _ -> str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name @@ -408,7 +408,7 @@ let pp_logical_ind packet = fnl () let pp_singleton kn packet = - let name = pp_global Type (IndRef (kn,0)) in + let name = pp_global Type (IndRef (mind_of_kn kn,0)) in let l = rename_tvars keywords packet.ip_vars in hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ @@ -416,7 +416,7 @@ let pp_singleton kn packet = pr_id packet.ip_consnames.(0))) let pp_record kn projs ip_equiv packet = - let name = pp_global Type (IndRef (kn,0)) in + let name = pp_global Type (IndRef (mind_of_kn kn,0)) in let projnames = List.map (pp_global Term) projs in let l = List.combine projnames packet.ip_types.(0) in let pl = rename_tvars keywords packet.ip_vars in @@ -438,20 +438,20 @@ let pp_ind co kn ind = let init= ref (str "type ") in let names = Array.mapi (fun i p -> if p.ip_logical then mt () else - pp_global Type (IndRef (kn,i))) + pp_global Type (IndRef (mind_of_kn kn,i))) ind.ind_packets in let cnames = Array.mapi (fun i p -> if p.ip_logical then [||] else - Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((kn,i),j+1))) + Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((mind_of_kn kn,i),j+1))) p.ip_types) ind.ind_packets in let rec pp i = if i >= Array.length ind.ind_packets then mt () else - let ip = (kn,i) in + let ip = (mind_of_kn kn,i) in let ip_equiv = ind.ind_equiv, i in let p = ind.ind_packets.(i) in if is_custom (IndRef ip) then pp (i+1) @@ -601,12 +601,12 @@ and pp_module_type ol = function let name = pp_modname (MPbound mbid) in let def = pp_module_type None mt' in str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def - | MTsig (msid, sign) -> + | MTsig (mp1, sign) -> let tvm = top_visible_mp () in - let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in + let mp = match ol with None -> mp1 | Some l -> MPdot (tvm,l) in (* References in [sign] are in short form (relative to [msid]). In push_visible, [msid-->mp] is added to the current subst. *) - push_visible mp (Some msid); + push_visible mp (Some mp1); let l = map_succeed pp_specif sign in pop_visible (); str "sig " ++ fnl () ++ @@ -684,9 +684,9 @@ and pp_module_expr ol = function str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MEapply (me, me') -> pp_module_expr None me ++ str "(" ++ pp_module_expr None me' ++ str ")" - | MEstruct (msid, sel) -> + | MEstruct (mp, sel) -> let tvm = top_visible_mp () in - let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in + let mp = match ol with None -> mp | Some l -> MPdot (tvm,l) in (* No need to update the subst with [Some msid] below : names are already in long form (see [subst_structure] in [Extract_env]). *) push_visible mp None; diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 9451188aaf..043bf0fe75 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -31,13 +31,13 @@ let occur_kn_in_ref kn = function let modpath_of_r = function | ConstRef kn -> con_modpath kn | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> modpath kn + | ConstructRef ((kn,_),_) -> mind_modpath kn | VarRef _ -> assert false let label_of_r = function | ConstRef kn -> con_label kn | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> label kn + | ConstructRef ((kn,_),_) -> mind_label kn | VarRef _ -> assert false let rec base_mp = function @@ -93,15 +93,34 @@ let rec parse_labels ll = function let labels_of_mp mp = parse_labels [] mp +let rec parse_labels2 ll mp1 = function + | mp when mp1=mp -> mp,ll + | MPdot (mp,l) -> parse_labels (l::ll) mp + | mp -> mp,ll + let labels_of_ref r = - let mp,_,l = + let mp_top = fst(Lib.current_prefix()) in + let mp,_,l = + match r with + ConstRef con -> repr_con con + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> repr_mind kn + | VarRef _ -> assert false + 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_kn kn + | ConstructRef ((kn,_),_) -> repr_mind kn | VarRef _ -> assert false - in - parse_labels [l] mp + in mp1,l + let rec add_labels_mp mp = function | [] -> mp @@ -127,10 +146,10 @@ let lookup_type kn = Cmap.find kn !types (*s Inductives table. *) -let inductives = ref (KNmap.empty : (mutual_inductive_body * ml_ind) KNmap.t) -let init_inductives () = inductives := KNmap.empty -let add_ind kn mib ml_ind = inductives := KNmap.add kn (mib,ml_ind) !inductives -let lookup_ind kn = KNmap.find kn !inductives +let inductives = ref (Mindmap.empty : (mutual_inductive_body * ml_ind) Mindmap.t) +let init_inductives () = inductives := Mindmap.empty +let add_ind kn mib ml_ind = inductives := Mindmap.add kn (mib,ml_ind) !inductives +let lookup_ind kn = Mindmap.find kn !inductives (*s Recursors table. *) @@ -138,7 +157,7 @@ let recursors = ref Cset.empty let init_recursors () = recursors := Cset.empty let add_recursors env kn = - let make_kn id = make_con (modpath kn) empty_dirpath (label_of_id id) in + let make_kn id = make_con (mind_modpath kn) empty_dirpath (label_of_id id) in let mib = Environ.lookup_mind kn env in Array.iter (fun mip -> @@ -305,7 +324,13 @@ let error_record r = let check_loaded_modfile mp = match base_mp mp with | MPfile dp -> if not (Library.library_is_loaded dp) then - err (str ("Please load library "^(string_of_dirpath dp^" first."))) + let mp1 = (fst(Lib.current_prefix())) in + let rec find_prefix = function + |MPfile dp1 when dp=dp1 -> () + |MPdot(mp,_) -> find_prefix mp + |MPbound(_) -> () + | _ -> err (str ("Please load library "^(string_of_dirpath dp^" first."))) + in find_prefix mp1 | _ -> () let info_file f = @@ -450,7 +475,7 @@ let (inline_extraction,_) = load_function = (fun _ (_,(b,l)) -> add_inline_entries b l); classify_function = (fun o -> Substitute o); subst_function = - (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))) + (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))) } let _ = declare_summary "Extraction Inline" @@ -528,7 +553,7 @@ let (blacklist_extraction,_) = cache_function = (fun (_,l) -> add_blacklist_entries l); load_function = (fun _ (_,l) -> add_blacklist_entries l); classify_function = (fun o -> Libobject.Keep o); - subst_function = (fun (_,_,x) -> x) + subst_function = (fun (_,x) -> x) } let _ = declare_summary "Extraction Blacklist" @@ -585,7 +610,7 @@ let (in_customs,_) = load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s); classify_function = (fun o -> Substitute o); subst_function = - (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str)) + (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str)) } let _ = declare_summary "ML extractions" diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 42ed6eef01..512ecca743 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -38,7 +38,7 @@ val info_file : string -> unit (*s utilities about [module_path] and [kernel_names] and [global_reference] *) -val occur_kn_in_ref : kernel_name -> global_reference -> bool +val occur_kn_in_ref : mutual_inductive -> global_reference -> bool val modpath_of_r : global_reference -> module_path val label_of_r : global_reference -> label val current_toplevel : unit -> module_path @@ -56,6 +56,7 @@ 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 *) @@ -65,10 +66,10 @@ val lookup_term : constant -> ml_decl val add_type : constant -> ml_schema -> unit val lookup_type : constant -> ml_schema -val add_ind : kernel_name -> mutual_inductive_body -> ml_ind -> unit -val lookup_ind : kernel_name -> mutual_inductive_body * ml_ind +val add_ind : mutual_inductive -> mutual_inductive_body -> ml_ind -> unit +val lookup_ind : mutual_inductive -> mutual_inductive_body * ml_ind -val add_recursors : Environ.env -> kernel_name -> unit +val add_recursors : Environ.env -> mutual_inductive -> unit val is_recursor : global_reference -> bool val add_projection : int -> constant -> unit diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index 7ac5f4e89e..91c0ca21ec 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -60,7 +60,7 @@ let _ = let load_addfield _ = () let cache_addfield (_,(typ,th)) = th_tab := Gmap.add typ th !th_tab -let subst_addfield (_,subst,(typ,th as obj)) = +let subst_addfield (subst,(typ,th as obj)) = let typ' = subst_mps subst typ in let th' = subst_mps subst th in if typ' == typ && th' == th then obj else diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 600a9123b4..19a884323e 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -317,9 +317,9 @@ let cache_Function (_,finfos) = let load_Function _ = cache_Function let open_Function _ = cache_Function -let subst_Function (_,subst,finfos) = +let subst_Function (subst,finfos) = let do_subst_con c = fst (Mod_subst.subst_con subst c) - and do_subst_ind (kn,i) = (Mod_subst.subst_kn subst kn,i) + and do_subst_ind (kn,i) = (Mod_subst.subst_ind subst kn,i) in let function_constant' = do_subst_con finfos.function_constant in let graph_ind' = do_subst_ind finfos.graph_ind in diff --git a/plugins/interface/centaur.ml4 b/plugins/interface/centaur.ml4 index e7084fbb00..07f32b6d43 100644 --- a/plugins/interface/centaur.ml4 +++ b/plugins/interface/centaur.ml4 @@ -416,7 +416,7 @@ let inspect n = | (sp,kn), "MUTUALINDUCTIVE" -> add_search2 (Nametab.locate (qualid_of_path sp)) (Pretyping.Default.understand Evd.empty (Global.env()) - (RRef(dummy_loc, IndRef(kn,0)))) + (RRef(dummy_loc, IndRef((mind_of_kn kn),0)))) | _ -> failwith ("unexpected value 1 for "^ (string_of_id (basename (fst oname))))) | _ -> failwith "unexpected value") diff --git a/plugins/interface/name_to_ast.ml b/plugins/interface/name_to_ast.ml index ef61a8202d..142116adea 100644 --- a/plugins/interface/name_to_ast.ml +++ b/plugins/interface/name_to_ast.ml @@ -176,10 +176,11 @@ let inductive_to_ast_list sp = let leaf_entry_to_ast_list ((sp,kn),lobj) = let tag = object_tag lobj in + let con = constant_of_kn kn in match tag with | "VARIABLE" -> variable_to_ast_list (basename sp) - | "CONSTANT" -> constant_to_ast_list (constant_of_kn kn) - | "INDUCTIVE" -> inductive_to_ast_list kn + | "CONSTANT" -> constant_to_ast_list con + | "INDUCTIVE" -> inductive_to_ast_list (mind_of_kn kn) | s -> errorlabstrm "print" (str ("printing of unrecognized object " ^ diff --git a/plugins/interface/name_to_ast.mli b/plugins/interface/name_to_ast.mli index a532604f59..db2555550e 100644 --- a/plugins/interface/name_to_ast.mli +++ b/plugins/interface/name_to_ast.mli @@ -2,4 +2,4 @@ val name_to_ast : Libnames.reference -> Vernacexpr.vernac_expr;; val inductive_to_ast_list : Names.mutual_inductive -> Vernacexpr.vernac_expr list;; val constant_to_ast_list : Names.constant -> Vernacexpr.vernac_expr list;; val variable_to_ast_list : Names.variable -> Vernacexpr.vernac_expr list;; -val leaf_entry_to_ast_list : (Libnames.full_path * Names.mutual_inductive) * Libobject.obj -> Vernacexpr.vernac_expr list;; +val leaf_entry_to_ast_list : (Libnames.full_path * Names.kernel_name) * Libobject.obj -> Vernacexpr.vernac_expr list;; diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 6ee12ebcb3..c0b5542ee5 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -258,7 +258,7 @@ let subst_theory subst th = } -let subst_th (_,subst,(c,th as obj)) = +let subst_th (subst,(c,th as obj)) = let c' = subst_mps subst c in let th' = subst_theory subst th in if c' == c && th' == th then obj else diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index a930fee17b..e85c12c591 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -400,7 +400,7 @@ let add_entry (sp,_kn) e = from_name := Spmap.add sp e !from_name -let subst_th (_,subst,th) = +let subst_th (subst,th) = let c' = subst_mps subst th.ring_carrier in let eq' = subst_mps subst th.ring_req in let set' = subst_mps subst th.ring_setoid in @@ -980,7 +980,7 @@ let add_field_entry (sp,_kn) e = field_from_relation := Cmap.add e.field_req e !field_from_relation; field_from_name := Spmap.add sp e !field_from_name -let subst_th (_,subst,th) = +let subst_th (subst,th) = let c' = subst_mps subst th.field_carrier in let eq' = subst_mps subst th.field_req in let thm1' = subst_mps subst th.field_ok in diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index d54bbee4e3..4eb05df74d 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -484,7 +484,7 @@ let check_and_adjust_constructor env ind cstrs = function | PatCstr (loc,((_,i) as cstr),args,alias) as pat -> (* Check it is constructor of the right type *) let ind' = inductive_of_constructor cstr in - if Closure.mind_equiv env ind' ind then + if Names.eq_ind ind' ind then (* Check the constructor has the right number of args *) let ci = cstrs.(i-1) in let nb_args_constr = ci.cs_nargs in diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 76a8a03221..f617c1008d 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -155,7 +155,7 @@ let cache (_, (infos, tac)) = let load (_, (_, tac)) = set_default_tactic tac -let subst (_, s, (infos, tac)) = +let subst (s, (infos, tac)) = (infos, Tacinterp.subst_tactic s tac) let (input,output) = diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml index f60abaf855..19473dfa69 100644 --- a/plugins/syntax/ascii_syntax.ml +++ b/plugins/syntax/ascii_syntax.ml @@ -21,7 +21,7 @@ open Bigint exception Non_closed_ascii let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) -let make_kn dir id = Libnames.encode_kn (make_dir dir) (id_of_string id) +let make_kn dir id = Libnames.encode_mind (make_dir dir) (id_of_string id) let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id) let ascii_module = ["Coq";"Strings";"Ascii"] diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index e58618219b..21b7115b62 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -24,7 +24,7 @@ let make_path dir id = Libnames.make_path (make_dir dir) (Names.id_of_string id) (* copied on g_zsyntax.ml, where it is said to be a temporary hack*) (* takes a path an identifier in the form of a string list and a string, returns a kernel_name *) -let make_kn dir id = Libnames.encode_kn (make_dir dir) (Names.id_of_string id) +let make_kn dir id = Libnames.encode_mind (make_dir dir) (Names.id_of_string id) (* int31 stuff *) @@ -50,9 +50,10 @@ let zn2z_WW = ConstructRef ((zn2z_id "zn2z",0),2) let bigN_module = ["Coq"; "Numbers"; "Natural"; "BigN"; "BigN" ] let bigN_path = make_path (bigN_module@["BigN"]) "t" (* big ugly hack *) -let bigN_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigN_module)), - Names.mk_label "BigN")), - [], Names.id_of_string id) : Names.kernel_name) +let bigN_id id = let kn = + ((Names.MPdot ((Names.MPfile (make_dir bigN_module)), + Names.mk_label "BigN")), + [], Names.id_of_string id) in (Obj.magic (kn,kn) : Names.mutual_inductive) let bigN_scope = "bigN_scope" (* number of inlined level of bigN (actually the level 0 to n_inlined-1 are inlined) *) @@ -81,9 +82,9 @@ let bigN_constructor = let bigZ_module = ["Coq"; "Numbers"; "Integer"; "BigZ"; "BigZ" ] let bigZ_path = make_path (bigZ_module@["BigZ"]) "t" (* big ugly hack bis *) -let bigZ_id id = (Obj.magic ((Names.MPdot ((Names.MPfile (make_dir bigZ_module)), +let bigZ_id id = let kn = ((Names.MPdot ((Names.MPfile (make_dir bigZ_module)), Names.mk_label "BigZ")), - [], Names.id_of_string id) : Names.kernel_name) + [], Names.id_of_string id) in (Obj.magic (kn,kn): Names.mutual_inductive) let bigZ_scope = "bigZ_scope" let bigZ_pos = ConstructRef ((bigZ_id "t_",0),1) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index a10c76013f..f6afd080f4 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -31,7 +31,7 @@ let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id) let positive_path = make_path positive_module "positive" (* TODO: temporary hack *) -let make_kn dir id = Libnames.encode_kn dir id +let make_kn dir id = Libnames.encode_mind dir id let positive_kn = make_kn (make_dir positive_module) (id_of_string "positive") diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 5bb7635b9d..7706a3eb59 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -80,7 +80,7 @@ let get_uri_of_var v pvars = type tag = Constant of Names.constant - | Inductive of Names.kernel_name + | Inductive of Names.mutual_inductive | Variable of Names.kernel_name ;; @@ -165,7 +165,7 @@ let token_list_of_kernel_name tag = N.id_of_label (N.con_label con), Lib.remove_section_part (LN.ConstRef con) | Inductive kn -> - N.id_of_label (N.label kn), + N.id_of_label (N.mind_label kn), Lib.remove_section_part (LN.IndRef (kn,0)) in token_list_of_path dir id (etag_of_tag tag) diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index a46500b89c..294f5154d3 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -629,7 +629,7 @@ let _ = let _ = Declare.set_xml_declare_inductive (function (isrecord,(sp,kn)) -> - print false (Libnames.IndRef (kn,0)) (kind_of_inductive isrecord kn) + print false (Libnames.IndRef (Names.mind_of_kn kn,0)) (kind_of_inductive isrecord (Names.mind_of_kn kn)) xml_library_root) ;; |