diff options
Diffstat (limited to 'contrib/extraction')
| -rw-r--r-- | contrib/extraction/extraction.ml | 23 | ||||
| -rw-r--r-- | contrib/extraction/table.ml | 9 | ||||
| -rw-r--r-- | contrib/extraction/table.mli | 5 |
3 files changed, 18 insertions, 19 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 5a192b62e..3fa318e7e 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -31,10 +31,6 @@ open Mlutil exception I of inductive_info -(* A set of all inductive currently being computed, - to avoid loops in [extract_inductive] *) -let internal_call = ref KNset.empty - (* A set of all fixpoint functions currently being extracted *) let current_fixpoints = ref ([] : constant list) @@ -303,13 +299,15 @@ and extract_type_scheme env db c p = (*S Extraction of an inductive type. *) and extract_ind env kn = (* kn is supposed to be in long form *) - try - if KNset.mem kn !internal_call then lookup_ind kn (* Already started. *) - else if visible_kn kn then lookup_ind kn (* Standard situation. *) - else raise Not_found (* Never trust the table for a internal kn. *) + let mib = Environ.lookup_mind kn env in + try + (* For a same kn, we can get various bodies due to module substitutions. + We hence check that the mib has not changed from recording + time to retrieving time. Ideally we should also check the env. *) + let (mib0,ml_ind) = lookup_ind kn in + if not (mib = mib0) then raise Not_found; + ml_ind with Not_found -> - internal_call := KNset.add kn !internal_call; - let mib = Environ.lookup_mind kn env in (* 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; @@ -335,7 +333,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) ip_types = t }) mib.mind_packets in - add_ind kn + add_ind kn mib {ind_info = Standard; ind_nparams = npar; ind_packets = packets; @@ -425,8 +423,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) ind_packets = packets; ind_equiv = mib.mind_equiv} in - add_ind kn i; - internal_call := KNset.remove kn !internal_call; + add_ind kn mib i; i (*s [extract_type_cons] extracts the type of an inductive diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 47a0977a5..22778ccff 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -77,9 +77,9 @@ let lookup_type kn = Cmap.find kn !types (*s Inductives table. *) -let inductives = ref (KNmap.empty : ml_ind KNmap.t) +let inductives = ref (KNmap.empty : (mutual_inductive_body * ml_ind) KNmap.t) let init_inductives () = inductives := KNmap.empty -let add_ind kn m = inductives := KNmap.add kn m !inductives +let add_ind kn mib ml_ind = inductives := KNmap.add kn (mib,ml_ind) !inductives let lookup_ind kn = KNmap.find kn !inductives (*s Recursors table. *) @@ -124,8 +124,9 @@ let reset_tables () = let id_of_global = function | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l - | IndRef (kn,i) -> (lookup_ind kn).ind_packets.(i).ip_typename - | ConstructRef ((kn,i),j) -> (lookup_ind kn).ind_packets.(i).ip_consnames.(j-1) + | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename + | ConstructRef ((kn,i),j) -> + (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1) | _ -> assert false let pr_global r = pr_id (id_of_global r) diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index 6be869e59..cc793b1a1 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -11,6 +11,7 @@ open Names open Libnames open Miniml +open Declarations val id_of_global : global_reference -> identifier @@ -55,8 +56,8 @@ val lookup_term : constant -> ml_decl val add_type : constant -> ml_schema -> unit val lookup_type : constant -> ml_schema -val add_ind : kernel_name -> ml_ind -> unit -val lookup_ind : kernel_name -> ml_ind +val add_ind : kernel_name -> mutual_inductive_body -> ml_ind -> unit +val lookup_ind : kernel_name -> mutual_inductive_body * ml_ind val add_recursors : Environ.env -> kernel_name -> unit val is_recursor : global_reference -> bool |