From 499a11a45b5711d4eaabe84a80f0ad3ae539d500 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 8 May 2013 17:47:10 +0200 Subject: Imported Upstream version 8.4pl2dfsg --- kernel/csymtable.ml | 4 +++- kernel/mod_subst.ml | 25 +++++++++++++++---------- kernel/modops.ml | 2 +- kernel/modops.mli | 3 ++- kernel/names.ml | 10 +++++++--- kernel/pre_env.ml | 2 +- kernel/safe_typing.ml | 5 +++-- kernel/subtyping.ml | 12 ++++++++---- 8 files changed, 40 insertions(+), 23 deletions(-) (limited to 'kernel') diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 8d09cbd7..9c9f6a57 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -190,7 +190,9 @@ and eval_to_patch env (buff,pl,fv) = and val_of_constr env c = let (_,fun_code,_ as ccfv) = try compile env c - with e -> print_string "can not compile \n";Format.print_flush();raise e in + with reraise -> + print_string "can not compile \n";Format.print_flush();raise reraise + in eval_to_patch env (to_memory ccfv) let set_transparent_const kn = diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 15a48e1c..9aeaf110 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -83,13 +83,14 @@ let string_of_hint = function | Equiv kn -> string_of_kn kn let debug_string_of_delta resolve = - let kn_to_string kn hint s = - s^", "^(string_of_kn kn)^"=>"^(string_of_hint hint) + let kn_to_string kn hint l = + (string_of_kn kn ^ "=>" ^ string_of_hint hint) :: l in - let mp_to_string mp mp' s = - s^", "^(string_of_mp mp)^"=>"^(string_of_mp mp') + let mp_to_string mp mp' l = + (string_of_mp mp ^ "=>" ^ string_of_mp mp') :: l in - Deltamap.fold mp_to_string kn_to_string resolve "" + let l = Deltamap.fold mp_to_string kn_to_string resolve [] in + String.concat ", " (List.rev l) let list_contents sub = let one_pair (mp,reso) = (string_of_mp mp,debug_string_of_delta reso) in @@ -173,7 +174,7 @@ let solve_delta_kn resolve kn = let kn_of_delta resolve kn = try solve_delta_kn resolve kn - with _ -> kn + with e when Errors.noncritical e -> kn let constant_of_delta_kn resolve kn = constant_of_kn_equiv kn (kn_of_delta resolve kn) @@ -182,7 +183,7 @@ let gen_of_delta resolve x kn fix_can = try let new_kn = solve_delta_kn resolve kn in if kn == new_kn then x else fix_can new_kn - with _ -> x + with e when Errors.noncritical e -> x let constant_of_delta resolve con = let kn = user_con con in @@ -223,8 +224,10 @@ let constant_of_delta_with_inline resolve con = let kn1,kn2 = canonical_con con,user_con con in try find_inline_of_delta kn2 resolve with Not_found -> - try find_inline_of_delta kn1 resolve - with Not_found -> None + if kn1 == kn2 then None + else + try find_inline_of_delta kn1 resolve + with Not_found -> None let subst_mp0 sub mp = (* 's like subst *) let rec aux mp = @@ -272,7 +275,9 @@ type sideconstantsubst = | Canonical let gen_subst_mp f sub mp1 mp2 = - match subst_mp0 sub mp1, subst_mp0 sub mp2 with + let o1 = subst_mp0 sub mp1 in + let o2 = if mp1 == mp2 then o1 else subst_mp0 sub mp2 in + match o1, o2 with | None, None -> raise No_subst | Some (mp',resolve), None -> User, (f mp' mp2), resolve | None, Some (mp',resolve) -> Canonical, (f mp1 mp'), resolve diff --git a/kernel/modops.ml b/kernel/modops.ml index af32288c..a81f868e 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -33,7 +33,7 @@ type signature_mismatch_error = | NotConvertibleInductiveField of identifier | NotConvertibleConstructorField of identifier | NotConvertibleBodyField - | NotConvertibleTypeField + | NotConvertibleTypeField of env * types * types | NotSameConstructorNamesField | NotSameInductiveNameInBlockField | FiniteInductiveFieldExpected of bool diff --git a/kernel/modops.mli b/kernel/modops.mli index d03d61bd..daea3258 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -9,6 +9,7 @@ open Util open Names open Univ +open Term open Environ open Declarations open Entries @@ -60,7 +61,7 @@ type signature_mismatch_error = | NotConvertibleInductiveField of identifier | NotConvertibleConstructorField of identifier | NotConvertibleBodyField - | NotConvertibleTypeField + | NotConvertibleTypeField of env * types * types | NotSameConstructorNamesField | NotSameInductiveNameInBlockField | FiniteInductiveFieldExpected of bool diff --git a/kernel/names.ml b/kernel/names.ml index 17bda124..8c228404 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -205,7 +205,9 @@ type constant = kernel_name*kernel_name let constant_of_kn kn = (kn,kn) let constant_of_kn_equiv kn1 kn2 = (kn1,kn2) let make_con mp dir l = constant_of_kn (mp,dir,l) -let make_con_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l)) +let make_con_equiv mp1 mp2 dir l = + if mp1 == mp2 then make_con mp1 dir l + else ((mp1,dir,l),(mp2,dir,l)) let canonical_con con = snd con let user_con con = fst con let repr_con con = fst con @@ -263,8 +265,10 @@ let constr_modpath c = ind_modpath (fst c) let mind_of_kn kn = (kn,kn) let mind_of_kn_equiv kn1 kn2 = (kn1,kn2) -let make_mind mp dir l = ((mp,dir,l),(mp,dir,l)) -let make_mind_equiv mp1 mp2 dir l = ((mp1,dir,l),(mp2,dir,l)) +let make_mind mp dir l = mind_of_kn (mp,dir,l) +let make_mind_equiv mp1 mp2 dir l = + if mp1 == mp2 then make_mind mp1 dir l + else ((mp1,dir,l),(mp2,dir,l)) let canonical_mind mind = snd mind let user_mind mind = fst mind let repr_mind mind = fst mind diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 6c08c34c..f0a3292c 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -90,7 +90,7 @@ let push_rel d env = let lookup_rel_val n env = try List.nth env.env_rel_val (n - 1) - with _ -> raise Not_found + with e when Errors.noncritical e -> raise Not_found let env_of_rel n env = { env with diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 1d606782..ec891e13 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -477,7 +477,7 @@ let end_module l restype senv = in let str = match sign with | SEBstruct(str_l) -> str_l - | _ -> error ("You cannot Include a high-order structure.") + | _ -> error ("You cannot Include a higher-order structure.") in let senv = update_resolver (add_delta_resolver resolver) senv in @@ -873,7 +873,8 @@ end = struct let k = key_of_lazy_constr k in let access key = try (Lazy.force table).(key) - with _ -> error "Error while retrieving an opaque body" + with e when Errors.noncritical e -> + error "Error while retrieving an opaque body" in match load_proof with | Flags.Force -> diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index e2c5f48c..c809572a 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -219,6 +219,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let check_conv cst f = check_conv_error error cst f in let check_type cst env t1 t2 = + let err = NotConvertibleTypeField (env, t1, t2) in + (* If the type of a constant is generated, it may mention non-variable algebraic universes that the general conversion algorithm is not ready to handle. Anyway, generated types of @@ -257,12 +259,12 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = (the user has to use an explicit type in the interface *) error NoTypeConstraintExpected with NotArity -> - error NotConvertibleTypeField end + error err end | _ -> t1,t2 else (t1,t2) in - check_conv NotConvertibleTypeField cst conv_leq env t1 t2 + check_conv err cst conv_leq env t1 t2 in match info1 with @@ -301,7 +303,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = if constant_has_body cb2 then error DefinitionFieldExpected; let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in let typ2 = Typeops.type_of_constant_type env cb2.const_type in - check_conv NotConvertibleTypeField cst conv_leq env arity1 typ2 + let error = NotConvertibleTypeField (env, arity1, typ2) in + check_conv error cst conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> ignore (Util.error ( "The kernel does not recognize yet that a parameter can be " ^ @@ -312,7 +315,8 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = if constant_has_body cb2 then error DefinitionFieldExpected; let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in let ty2 = Typeops.type_of_constant_type env cb2.const_type in - check_conv NotConvertibleTypeField cst conv env ty1 ty2 + let error = NotConvertibleTypeField (env, ty1, ty2) in + check_conv error cst conv env ty1 ty2 let rec check_modules cst env msb1 msb2 subst1 subst2 = let mty1 = module_type_of_module None msb1 in -- cgit v1.2.3