aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/closure.ml7
-rw-r--r--checker/closure.mli1
-rw-r--r--checker/declarations.ml63
-rw-r--r--checker/declarations.mli1
-rw-r--r--checker/environ.ml21
-rw-r--r--checker/environ.mli3
-rw-r--r--checker/mod_checking.ml33
-rw-r--r--checker/modops.ml2
-rw-r--r--checker/reduction.ml2
-rw-r--r--checker/subtyping.ml6
-rw-r--r--checker/term.ml6
-rw-r--r--kernel/names.ml4
-rw-r--r--kernel/names.mli7
13 files changed, 112 insertions, 44 deletions
diff --git a/checker/closure.ml b/checker/closure.ml
index 054057d1f..27848efa7 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -376,7 +376,12 @@ let defined_rels flags env =
(rel_context env) ~init:(0,[])
(* else (0,[])*)
-let mind_equiv_infos info = eq_ind
+let mind_equiv_infos info = mind_equiv info.i_env
+
+let eq_table_key k1 k2 =
+ match k1,k2 with
+ | ConstKey con1 ,ConstKey con2 -> eq_con_chk con1 con2
+ | _,_ -> k1=k2
let create mk_cl flgs env =
{ i_flags = flgs;
diff --git a/checker/closure.mli b/checker/closure.mli
index ada7ded1e..bc0704d91 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -175,6 +175,7 @@ val unfold_reference : clos_infos -> table_key -> fconstr option
(* [mind_equiv] checks whether two inductive types are intentionally equal *)
val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool
+val eq_table_key : table_key -> table_key -> bool
(************************************************************************)
(*i This is for lazy debug *)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 2a5d3114c..699f6c90e 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -492,21 +492,30 @@ let val_substituted val_a =
[|[|val_a|];[|val_list val_subst;val_a|]|])
let from_val a = ref (LSval a)
-
+
+let rec replace_mp_in_mp mpfrom mpto mp =
+ match mp with
+ | _ when mp = mpfrom -> mpto
+ | MPdot (mp1,l) ->
+ let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
+ if mp1==mp1' then mp
+ else MPdot (mp1',l)
+ | _ -> mp
+
+let rec mp_in_mp mp mp1 =
+ match mp1 with
+ | _ when mp1 = mp -> true
+ | MPdot (mp2,l) -> mp_in_mp mp mp2
+ | _ -> false
+
let mp_in_key mp key =
- let rec mp_rec mp1 =
- match mp1 with
- | _ when mp1 = mp -> true
- | MPdot (mp2,l) -> mp_rec mp2
- | _ -> false
- in
- match key with
+ match key with
| MP mp1 ->
- mp_rec mp1
+ mp_in_mp mp mp1
| KN kn ->
let mp1,dir,l = repr_kn kn in
- mp_rec mp1
-
+ mp_in_mp mp mp1
+
let subset_prefixed_by mp resolver =
let prefixmp key hint resolv =
if mp_in_key mp key then
@@ -583,10 +592,23 @@ let add_delta_resolver resolver1 resolver2 =
Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2)
resolver2
+let substition_prefixed_by k mp subst =
+ let prefixmp key (mp_to,reso) sub =
+ match key with
+ | MPI mpk ->
+ if mp_in_mp mp mpk && mp <> mpk then
+ let new_key = replace_mp_in_mp mp k mpk in
+ Umap.add (MPI new_key) (mp_to,reso) sub
+ else
+ sub
+ | _ -> sub
+ in
+ Umap.fold prefixmp subst empty_subst
+
let join (subst1 : substitution) (subst2 : substitution) =
- let apply_subst (sub : substitution) key (mp,resolve) =
+ let apply_subst key (mp,resolve) res =
let mp',resolve' =
- match subst_mp0 sub mp with
+ match subst_mp0 subst2 mp with
None -> mp, None
| Some (mp',resolve') -> mp'
,Some resolve' in
@@ -594,15 +616,16 @@ let join (subst1 : substitution) (subst2 : substitution) =
match resolve' with
Some res ->
add_delta_resolver
- (subst_dom_codom_delta_resolver sub resolve)
- res
+ (subst_dom_codom_delta_resolver subst2 resolve) res
| None ->
- subst_codom_delta_resolver sub resolve
+ subst_codom_delta_resolver subst2 resolve
in
- mp',resolve'' in
- let subst = Umap.mapi (apply_subst subst2) subst1 in
- (Umap.fold Umap.add subst2 subst)
-
+ let k = match key with MBI mp -> MPbound mp | MPI mp -> mp in
+ let prefixed_subst = substition_prefixed_by k mp subst2 in
+ Umap.fold Umap.add prefixed_subst
+ (Umap.add key (mp',resolve'') res) in
+ let subst = Umap.fold apply_subst subst1 empty_subst in
+ (Umap.fold Umap.add subst2 subst)
let force fsubst r =
match !r with
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 8afe09dac..b39fd6f2f 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -199,6 +199,7 @@ val add_mp : module_path -> module_path -> substitution -> substitution
val map_mbid : mod_bound_id -> module_path -> substitution
val map_mp : module_path -> module_path -> substitution
val mp_in_delta : module_path -> delta_resolver -> bool
+val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
val subst_const_body : constant_body subst_fun
val subst_mind : mutual_inductive_body subst_fun
diff --git a/checker/environ.ml b/checker/environ.ml
index 3d14b995b..a72aae91d 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -7,6 +7,7 @@ open Declarations
type globals = {
env_constants : constant_body Cmap_env.t;
env_inductives : mutual_inductive_body Mindmap_env.t;
+ env_inductives_eq : kernel_name KNmap.t;
env_modules : module_body MPmap.t;
env_modtypes : module_type_body MPmap.t}
@@ -26,6 +27,7 @@ let empty_env = {
env_globals =
{ env_constants = Cmap_env.empty;
env_inductives = Mindmap_env.empty;
+ env_inductives_eq = KNmap.empty;
env_modules = MPmap.empty;
env_modtypes = MPmap.empty};
env_named_context = [];
@@ -142,14 +144,31 @@ let evaluable_constant cst env =
with Not_found | NotEvaluableConst _ -> false
(* Mutual Inductives *)
+let scrape_mind env kn=
+ try
+ KNmap.find kn env.env_globals.env_inductives_eq
+ with
+ Not_found -> kn
+
+let mind_equiv env (kn1,i1) (kn2,i2) =
+ i1 = i2 &&
+ scrape_mind env (user_mind kn1) = scrape_mind env (user_mind kn2)
+
+
let lookup_mind kn env =
Mindmap_env.find kn env.env_globals.env_inductives
let add_mind kn mib env =
let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
+ let kn1,kn2 = user_mind kn,canonical_mind kn in
+ let new_inds_eq = if kn1=kn2 then
+ env.env_globals.env_inductives_eq
+ else
+ KNmap.add kn1 kn2 env.env_globals.env_inductives_eq in
let new_globals =
{ env.env_globals with
- env_inductives = new_inds } in
+ env_inductives = new_inds;
+ env_inductives_eq = new_inds_eq} in
{ env with env_globals = new_globals }
diff --git a/checker/environ.mli b/checker/environ.mli
index 776698ed8..023acd0bf 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -6,6 +6,7 @@ open Term
type globals = {
env_constants : Declarations.constant_body Cmap_env.t;
env_inductives : Declarations.mutual_inductive_body Mindmap_env.t;
+ env_inductives_eq : kernel_name KNmap.t;
env_modules : Declarations.module_body MPmap.t;
env_modtypes : Declarations.module_type_body MPmap.t}
type stratification = {
@@ -57,6 +58,8 @@ val constant_opt_value : env -> constant -> constr option
val evaluable_constant : constant -> env -> bool
(* Inductives *)
+val mind_equiv : env -> inductive -> inductive -> bool
+
val lookup_mind :
mutual_inductive -> env -> Declarations.mutual_inductive_body
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index e95109fc5..23ba4893a 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -245,27 +245,30 @@ and check_module env mp mb =
match mb.mod_expr, mb.mod_type with
| None,mtb ->
let _ = check_modtype env mtb mb.mod_mp in ()
+ | Some mexpr, mtb when mtb==mexpr ->
+ let _ = check_modtype env mtb mb.mod_mp in ()
| Some mexpr, _ ->
- let sign = check_modexpr env mexpr mb.mod_mp in
- let _ = check_modtype env mb.mod_type mb.mod_mp in
+ let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in
+ let _ = check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in
check_subtypes env
{typ_mp=mp;
typ_expr=sign;
typ_expr_alg=None;
typ_constraints=Univ.Constraint.empty;
- typ_delta = empty_delta_resolver;}
+ typ_delta = mb.mod_delta;}
{typ_mp=mp;
typ_expr=mb.mod_type;
typ_expr_alg=None;
typ_constraints=Univ.Constraint.empty;
- typ_delta = empty_delta_resolver;};
+ typ_delta = mb.mod_delta;};
-and check_structure_field env mp lab = function
+and check_structure_field env mp lab res = function
| SFBconst cb ->
let c = make_con mp empty_dirpath lab in
check_constant_declaration env c cb
| SFBmind mib ->
let kn = make_mind mp empty_dirpath lab in
+ let kn = mind_of_delta res kn in
Indtypes.check_inductive env kn mib
| SFBmodule msb ->
let _= check_module env (MPdot(mp,lab)) msb in
@@ -274,17 +277,17 @@ and check_structure_field env mp lab = function
check_module_type env mty;
add_modtype (MPdot(mp,lab)) mty env
-and check_modexpr env mse mp_mse = match mse with
+and check_modexpr env mse mp_mse res = match mse with
| SEBident mp ->
let mb = lookup_module mp env in
(subst_and_strengthen mb mp_mse env).mod_type
| SEBfunctor (arg_id, mtb, body) ->
check_module_type env mtb ;
let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
- let sign = check_modexpr env' body mp_mse in
+ let sign = check_modexpr env' body mp_mse res in
SEBfunctor (arg_id, mtb, sign)
| SEBapply (f,m,cst) ->
- let sign = check_modexpr env f mp_mse in
+ let sign = check_modexpr env f mp_mse res in
let farg_id, farg_b, fbody_b = destr_functor env sign in
let mp =
try (path_of_mexpr m)
@@ -294,25 +297,25 @@ and check_modexpr env mse mp_mse = match mse with
check_subtypes env mtb farg_b;
(subst_struct_expr (map_mbid farg_id mp) fbody_b)
| SEBwith(mte, with_decl) ->
- let sign = check_modexpr env mte mp_mse in
+ let sign = check_modexpr env mte mp_mse res in
let sign = check_with env sign with_decl mp_mse in
sign
| SEBstruct(msb) ->
let _ = List.fold_left (fun env (lab,mb) ->
- check_structure_field env mp_mse lab mb) env msb in
+ check_structure_field env mp_mse lab res mb) env msb in
SEBstruct(msb)
-and check_modtype env mse mp_mse= match mse with
+and check_modtype env mse mp_mse res = match mse with
| SEBident mp ->
let mtb = lookup_modtype mp env in
mtb.typ_expr
| SEBfunctor (arg_id, mtb, body) ->
check_module_type env mtb;
let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
- let body = check_modtype env' body mp_mse in
+ let body = check_modtype env' body mp_mse res in
SEBfunctor(arg_id,mtb,body)
| SEBapply (f,m,cst) ->
- let sign = check_modtype env f mp_mse in
+ let sign = check_modtype env f mp_mse res in
let farg_id, farg_b, fbody_b = destr_functor env sign in
let mp =
try (path_of_mexpr m)
@@ -322,12 +325,12 @@ and check_modtype env mse mp_mse= match mse with
check_subtypes env mtb farg_b;
subst_struct_expr (map_mbid farg_id mp) fbody_b
| SEBwith(mte, with_decl) ->
- let sign = check_modtype env mte mp_mse in
+ let sign = check_modtype env mte mp_mse res in
let sign = check_with env sign with_decl mp_mse in
sign
| SEBstruct(msb) ->
let _ = List.fold_left (fun env (lab,mb) ->
- check_structure_field env mp_mse lab mb) env msb in
+ check_structure_field env mp_mse lab res mb) env msb in
SEBstruct(msb)
(*
diff --git a/checker/modops.ml b/checker/modops.ml
index e6428d5ab..f5d54c361 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -85,7 +85,7 @@ let rec add_signature mp sign resolver env =
let add_one env (l,elem) =
let kn = make_kn mp empty_dirpath l in
let con = constant_of_kn kn in
- let mind = mind_of_kn kn in
+ let mind = mind_of_delta resolver (mind_of_kn kn) in
match elem with
| SFBconst cb ->
(* let con = constant_of_delta resolver con in*)
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 776edb243..e00ece11a 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -254,7 +254,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
(* 2 constants, 2 local defined vars or 2 defined rels *)
| (FFlex fl1, FFlex fl2) ->
(try (* try first intensional equality *)
- if fl1 = fl2
+ if eq_table_key fl1 fl2
then convert_stacks univ infos lft1 lft2 v1 v2
else raise NotConvertible
with NotConvertible ->
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 9df49630c..d66a49546 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -361,8 +361,10 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv =
let check_subtypes env sup super =
(*if sup<>super then*)
- check_modtypes env (strengthen env sup sup.typ_mp) super empty_subst
- (map_mp super.typ_mp sup.typ_mp) false
+ let env = add_module
+ (module_body_of_type sup.typ_mp sup) env in
+ check_modtypes env (strengthen env sup sup.typ_mp) super empty_subst
+ (map_mp super.typ_mp sup.typ_mp) false
let check_equal env sup super =
(*if sup<>super then*)
diff --git a/checker/term.ml b/checker/term.ml
index 8d65bbe17..c39491ab5 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -487,9 +487,9 @@ let compare_constr f t1 t2 =
f h1 h2 & List.for_all2 f l1 l2
else false
| Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2
- | Const c1, Const c2 -> eq_constant c1 c2
- | Ind c1, Ind c2 -> c1 = c2
- | Construct c1, Construct c2 -> c1 = c2
+ | Const c1, Const c2 -> eq_con_chk c1 c2
+ | Ind c1, Ind c2 -> eq_ind_chk c1 c2
+ | Construct (c1,i1), Construct (c2,i2) -> i1=i2 && eq_ind_chk c1 c2
| Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2
| Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
diff --git a/kernel/names.ml b/kernel/names.ml
index dfa73e95a..463f47ca4 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -416,3 +416,7 @@ let eq_id_key ik1 ik2 =
ConstKey (_,kn1),
ConstKey (_,kn2) -> kn1=kn2
| a,b -> a=b
+
+let eq_con_chk (kn1,_) (kn2,_) = kn1=kn2
+let eq_mind_chk (kn1,_) (kn2,_) = kn1=kn2
+let eq_ind_chk (kn1,i1) (kn2,i2) = i1=i2&&eq_mind_chk kn1 kn2
diff --git a/kernel/names.mli b/kernel/names.mli
index 1c74fdee6..74cebd22a 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -229,3 +229,10 @@ type inv_rel_key = int (** index in the [rel_context] part of environment
type id_key = inv_rel_key tableKey
val eq_id_key : id_key -> id_key -> bool
+
+(*equalities on constant and inductive
+ names for the checker*)
+
+val eq_con_chk : constant -> constant -> bool
+val eq_ind_chk : inductive -> inductive -> bool
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 04:35:08 +0000