aboutsummaryrefslogtreecommitdiff
path: root/plugins/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/common.ml3
-rw-r--r--plugins/extraction/common.mli2
-rw-r--r--plugins/extraction/extract_env.ml124
-rw-r--r--plugins/extraction/extraction.ml21
-rw-r--r--plugins/extraction/extraction.mli2
-rw-r--r--plugins/extraction/haskell.ml6
-rw-r--r--plugins/extraction/miniml.mli4
-rw-r--r--plugins/extraction/mlutil.ml6
-rw-r--r--plugins/extraction/mlutil.mli2
-rw-r--r--plugins/extraction/modutil.ml21
-rw-r--r--plugins/extraction/ocaml.ml24
-rw-r--r--plugins/extraction/table.ml55
-rw-r--r--plugins/extraction/table.mli9
13 files changed, 150 insertions, 129 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 21:18:08 +0000