aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/closure.ml10
-rw-r--r--kernel/closure.mli3
-rw-r--r--kernel/declarations.ml5
-rw-r--r--kernel/declarations.mli4
-rw-r--r--kernel/indtypes.ml4
-rw-r--r--kernel/inductive.ml8
-rw-r--r--kernel/inductive.mli8
-rw-r--r--kernel/mod_typing.ml6
-rw-r--r--kernel/modops.ml53
-rw-r--r--kernel/modops.mli4
-rw-r--r--kernel/reduction.ml11
-rw-r--r--kernel/subtyping.ml63
12 files changed, 140 insertions, 39 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 463f6f21dd..2d30b2aa30 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -12,6 +12,7 @@ open Util
open Pp
open Term
open Names
+open Declarations
open Environ
open Esubst
@@ -385,6 +386,15 @@ let defined_rels flags env =
env ~init:(0,[])
(* else (0,[])*)
+
+let rec mind_equiv info kn1 kn2 =
+ kn1 = kn2 ||
+ match (lookup_mind kn1 info.i_env).mind_equiv with
+ Some kn1' -> mind_equiv info kn2 kn1'
+ | None -> match (lookup_mind kn2 info.i_env).mind_equiv with
+ Some kn2' -> mind_equiv info kn2' kn1
+ | None -> false
+
let create mk_cl flgs env =
{ i_flags = flgs;
i_repr = mk_cl;
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 826d58fbac..d3c5e5c59f 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -187,6 +187,9 @@ val whd_stack :
(* [unfold_reference] unfolds references in a [fconstr] *)
val unfold_reference : clos_infos -> table_key -> fconstr option
+(* [mind_equiv] checks whether two mutual inductives are intentionally equal *)
+val mind_equiv : clos_infos -> mutual_inductive -> mutual_inductive -> bool
+
(***********************************************************************)
(*i This is for lazy debug *)
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 67c0cb998f..8b11705970 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -84,7 +84,9 @@ type mutual_inductive_body = {
mind_hyps : section_context;
mind_packets : one_inductive_body array;
mind_constraints : constraints;
- mind_singl : constr option }
+ mind_singl : constr option;
+ mind_equiv : kernel_name option
+ }
(* TODO: should be changed to non-coping after Term.subst_mps *)
let subst_const_body sub cb =
@@ -119,6 +121,7 @@ let subst_mind sub mib =
mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
mind_constraints = mib.mind_constraints ;
mind_singl = option_app (Term.subst_mps sub) mib.mind_singl;
+ mind_equiv = option_app (subst_kn sub) mib.mind_equiv;
}
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 9ea7e20f82..574cb04fa6 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -76,7 +76,9 @@ type mutual_inductive_body = {
mind_hyps : section_context;
mind_packets : one_inductive_body array;
mind_constraints : constraints;
- mind_singl : constr option }
+ mind_singl : constr option;
+ mind_equiv : kernel_name option;
+ }
val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 036bce60bd..58a117bdcf 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -525,7 +525,9 @@ let build_inductive env env_ar finite inds recargs cst =
mind_hyps = hyps;
mind_packets = packets;
mind_constraints = cst;
- mind_singl = None }
+ mind_singl = None;
+ mind_equiv = None;
+ }
(***********************************************************************)
(***********************************************************************)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index cc2c37790f..605f11d673 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -697,6 +697,14 @@ let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
*)
(***********************************************************************)
+(* Scrape *)
+
+let rec scrape_mind env kn =
+ match (Environ.lookup_mind kn env).mind_equiv with
+ | None -> kn
+ | Some kn' -> scrape_mind env kn'
+
+(***********************************************************************)
(* Co-fixpoints. *)
exception CoFixGuardError of guard_error
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index f279eb79aa..a6ce7d42e8 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -44,8 +44,8 @@ val type_of_constructor : env -> constructor -> types
val arities_of_constructors : env -> inductive -> types array
(* Transforms inductive specification into types (in nf) *)
-val arities_of_specif :
- kernel_name -> mutual_inductive_body * one_inductive_body -> types array
+val arities_of_specif : mutual_inductive ->
+ mutual_inductive_body * one_inductive_body -> types array
(* [type_case_branches env (I,args) (p:A) c] computes useful types
about the following Cases expression:
@@ -62,6 +62,10 @@ val type_case_branches :
given inductive type. *)
val check_case_info : env -> inductive -> case_info -> unit
+(* Find the ultimate inductive in the mind_equiv chain *)
+
+val scrape_mind : env -> mutual_inductive -> mutual_inductive
+
(*s Guard conditions for fix and cofix-points. *)
val check_fix : env -> fixpoint -> unit
val check_cofix : env -> cofixpoint -> unit
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 5c4b00d94f..1eb74ffef6 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -32,6 +32,8 @@ let rec list_fold_map2 f e = function
let e'',t1',t2' = list_fold_map2 f e' t in
e'',h1'::t1',h2'::t2'
+let type_modpath env mp =
+ strengthen env (lookup_module mp env).mod_type mp
let rec translate_modtype env mte =
match mte with
@@ -100,7 +102,7 @@ and translate_module env is_definition me =
with
| Not_path -> error_declaration_not_path mexpr
in
- MEBident mp, (lookup_module mp env).mod_type
+ MEBident mp, type_modpath env mp
in
let mtb,mod_user_type =
match me.mod_entry_type with
@@ -118,7 +120,7 @@ and translate_module env is_definition me =
and translate_mexpr env mexpr = match mexpr with
| MEident mp ->
MEBident mp,
- (lookup_module mp env).mod_type
+ type_modpath env mp
| MEfunctor (arg_id, arg_e, body_expr) ->
let arg_b = translate_modtype env arg_e in
let env' = add_module (MPbound arg_id) (module_body_of_type arg_b) env in
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 1b0ff8ace7..ea8a2c4e27 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -55,7 +55,7 @@ let error_not_a_module s =
let rec scrape_modtype env = function
- | MTBident ln -> scrape_modtype env (lookup_modtype ln env)
+ | MTBident kn -> scrape_modtype env (lookup_modtype kn env)
| mtb -> mtb
@@ -79,7 +79,7 @@ let destr_functor = function
let rec check_modpath_equiv env mp1 mp2 =
- if mp1=mp2 then ();
+ if mp1=mp2 then () else
let mb1 = lookup_module mp1 env in
match mb1.mod_equiv with
| None ->
@@ -149,3 +149,52 @@ and add_module mp mb env =
| MTBfunsig _ -> env
+let strengthen_const env mp l cb = match cb.const_body with
+ | Some _ -> cb
+ | None -> {cb with const_body = Some (mkConst (make_kn mp empty_dirpath l))}
+
+let strengthen_mind env mp l mib = match mib.mind_equiv with
+ | Some _ -> mib
+ | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)}
+
+let rec strengthen_mtb env mp mtb = match scrape_modtype env mtb with
+ | MTBident _ -> anomaly "scrape_modtype does not work!"
+ | MTBfunsig _ -> mtb
+ | MTBsig (msid,sign) -> MTBsig (msid,strengthen_sig env msid sign mp)
+and strengthen_mod env mp (mtb,mpo) =
+ let mtb' = strengthen_mtb env mp mtb in
+ let mpo' = match mpo with
+ | Some _ -> mpo
+ | None -> Some mp
+ in
+ (mtb',mpo')
+and strengthen_sig env msid sign mp = match sign with
+ | [] -> []
+ | (l,SPBconst cb) :: rest ->
+ let item' = l,SPBconst (strengthen_const env mp l cb) in
+ let rest' = strengthen_sig env msid rest mp in
+ item'::rest'
+ | (l,SPBmind mib) :: rest ->
+ let item' = l,SPBmind (strengthen_mind env mp l mib) in
+ let rest' = strengthen_sig env msid rest mp in
+ item'::rest'
+ | (l,SPBmodule mb) :: rest ->
+ let mp' = MPdot (mp,l) in
+ let item' = l,SPBmodule (strengthen_mod env mp' mb) in
+ let env' = add_module
+ (MPdot (MPself msid,l))
+ (module_body_of_spec mb)
+ env
+ in
+ let rest' = strengthen_sig env' msid rest mp in
+ item'::rest'
+ | (l,SPBmodtype mty as item) :: rest ->
+ let env' = add_modtype
+ (make_kn (MPself msid) empty_dirpath l)
+ mty
+ env
+ in
+ let rest' = strengthen_sig env' msid rest mp in
+ item::rest'
+
+let strengthen env mtb mp = strengthen_mtb env mp mtb
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 2401447852..7cd22c57c8 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -51,6 +51,8 @@ val add_module :
val check_modpath_equiv : env -> module_path -> module_path -> unit
+val strengthen : env -> module_type_body -> module_path -> module_type_body
+
val error_existing_label : label -> 'a
val error_declaration_not_path : module_expr -> 'a
@@ -62,6 +64,8 @@ val error_not_a_functor : module_expr -> 'a
val error_incompatible_modtypes :
module_type_body -> module_type_body -> 'a
+val error_not_equal : module_path -> module_path -> 'a
+
val error_not_match : label -> specification_body -> 'a
val error_incompatible_labels : label -> label -> 'a
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4512546ae7..a452138fc1 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -244,14 +244,15 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
let u3 = convert_vect infos el1 el2 cl1 cl2 u2 in
convert_stacks infos lft1 lft2 v1 v2 u3
*)
- | (FInd op1, FInd op2) ->
- if op1 = op2 then
+ | (FInd (kn1,i1), FInd (kn2,i2)) ->
+ if i1 = i2 && mind_equiv infos kn1 kn2
+ then
convert_stacks infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
- | (FConstruct op1, FConstruct op2) ->
- if op1 = op2
- then
+ | (FConstruct ((kn1,i1),j1), FConstruct ((kn2,i2),j2)) ->
+ if i1 = i2 && j1 = j2 && mind_equiv infos kn1 kn2
+ then
convert_stacks infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 4b4ae17cfd..f62725c70d 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -103,8 +103,6 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
let cst = check_conv cst conv env p1.mind_nf_arity p2.mind_nf_arity in
cst
in
- (* this function uses mis_something and the others do not.
- Perhaps we should uniformize it at some point... *)
let check_cons_types i cst p1 p2 =
array_fold_left2
(fun cst t1 t2 -> check_conv cst conv env t1 t2)
@@ -113,28 +111,41 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
(arities_of_specif kn (mib2,p2))
in
let check f = if f mib1 <> f mib2 then error () in
- check (fun mib -> mib.mind_finite);
- check (fun mib -> mib.mind_ntypes);
- assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]);
- assert (Array.length mib1.mind_packets >= 1
+ check (fun mib -> mib.mind_finite);
+ check (fun mib -> mib.mind_ntypes);
+ assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]);
+ assert (Array.length mib1.mind_packets >= 1
&& Array.length mib2.mind_packets >= 1);
- check (fun mib -> mib.mind_packets.(0).mind_nparams);
- check (fun mib -> mib.mind_packets.(0).mind_params_ctxt);
- (* TODO: we should allow renaming of parameters at least ! *)
- let cst = match mib1.mind_singl, mib2.mind_singl with
- None, None -> cst
- | Some c1, Some c2 -> check_conv cst conv env c1 c2
- | _ -> error ()
- in
- (* we first check simple things *)
- let cst =
- array_fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets
- in
- (* and constructor types in the end *)
- let cst =
- array_fold_left2_i check_cons_types cst mib1.mind_packets mib2.mind_packets
- in
- cst
+
+ (* TODO: we should allow renaming of parameters at least ! *)
+ check (fun mib -> mib.mind_packets.(0).mind_nparams);
+ check (fun mib -> mib.mind_packets.(0).mind_params_ctxt);
+
+ begin
+ match mib2.mind_equiv with
+ | None -> ()
+ | Some kn2' ->
+ let kn2 = scrape_mind env kn2' in
+ let kn1 = match mib1.mind_equiv with
+ None -> kn
+ | Some kn1' -> scrape_mind env kn1'
+ in
+ if kn1 <> kn2 then error ()
+ end;
+ let cst = match mib1.mind_singl, mib2.mind_singl with
+ | None, None -> cst
+ | Some c1, Some c2 -> check_conv cst conv env c1 c2
+ | _ -> error ()
+ in
+ (* we first check simple things *)
+ let cst =
+ array_fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets
+ in
+ (* and constructor types in the end *)
+ let cst =
+ array_fold_left2_i check_cons_types cst mib1.mind_packets mib2.mind_packets
+ in
+ cst
let check_constant cst env msid1 l info1 cb2 spec2 =
let error () = error_not_match l spec2 in
@@ -172,12 +183,14 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
*)
let rec check_modules cst env msid1 l msb1 msb2 =
- let cst = check_modtypes cst env (fst msb1) (fst msb2) false in
+ let mp = (MPdot(MPself msid1,l)) in
+ let mty1 = strengthen env (fst msb1) mp in
+ let cst = check_modtypes cst env mty1 (fst msb2) false in
begin
match (snd msb1), (snd msb2) with
| _, None -> ()
| None, Some mp2 ->
- check_modpath_equiv env (MPdot(MPself msid1,l)) mp2
+ check_modpath_equiv env mp mp2
| Some mp1, Some mp2 ->
check_modpath_equiv env mp1 mp2
end;
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:52:22 +0000