From 300293c119981054c95182a90c829058530a6b6f Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 25 Dec 2011 13:19:42 +0100 Subject: Imported Upstream version 8.3.pl3 --- checker/check.ml | 2 +- checker/check_stat.ml | 2 +- checker/check_stat.mli | 2 +- checker/checker.ml | 2 +- checker/closure.ml | 2 +- checker/closure.mli | 2 +- checker/environ.ml | 21 +++++++++++++++ checker/environ.mli | 1 + checker/indtypes.ml | 2 +- checker/indtypes.mli | 2 +- checker/inductive.ml | 2 +- checker/inductive.mli | 2 +- checker/mod_checking.ml | 55 ++++++++++++++++++++++----------------- checker/modops.ml | 69 +++++++++++++++++++++---------------------------- checker/modops.mli | 8 +++--- checker/reduction.ml | 2 +- checker/reduction.mli | 2 +- checker/safe_typing.ml | 2 +- checker/safe_typing.mli | 2 +- checker/subtyping.ml | 15 +++++------ checker/subtyping.mli | 5 +++- checker/term.ml | 2 +- checker/type_errors.ml | 2 +- checker/type_errors.mli | 2 +- checker/typeops.ml | 2 +- checker/typeops.mli | 2 +- checker/validate.ml | 2 +- 27 files changed, 118 insertions(+), 96 deletions(-) (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index 9343d0b3..40119a7e 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* Declarations.module_type_body -> env -> env val shallow_add_module : module_path -> Declarations.module_body -> env -> env +val shallow_remove_module : module_path -> env -> env val lookup_module : module_path -> env -> Declarations.module_body val lookup_modtype : module_path -> env -> Declarations.module_type_body diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 2431f14e..277fed30 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* msb | _ -> error_not_a_module l in - let _ = (lookup_module mp1 env) in () + let (_:module_body) = (lookup_module mp1 env) in () | With_module_body (_::_,mp) -> let old = match spec with SFBmodule msb -> msb @@ -238,30 +238,39 @@ and check_with_aux_mod env mtb with_decl mp = | Reduction.NotConvertible -> error_with_incorrect l and check_module_type env mty = - let _ = check_modtype env mty.typ_expr mty.typ_mp mty.typ_delta in () + let (_:struct_expr_body) = + check_modtype env mty.typ_expr mty.typ_mp mty.typ_delta in + () and check_module env mp mb = match mb.mod_expr, mb.mod_type with | None,mtb -> - let _ = check_modtype env mtb mb.mod_mp mb.mod_delta in () + let (_:struct_expr_body) = + check_modtype env mtb mb.mod_mp mb.mod_delta in () | Some mexpr, mtb when mtb==mexpr -> - let _ = check_modtype env mtb mb.mod_mp mb.mod_delta in () + let (_:struct_expr_body) = + check_modtype env mtb mb.mod_mp mb.mod_delta in () | Some mexpr, _ -> 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 = mb.mod_delta;} - {typ_mp=mp; - typ_expr=mb.mod_type; - typ_expr_alg=None; - typ_constraints=Univ.Constraint.empty; - typ_delta = mb.mod_delta;}; - + let (_:struct_expr_body) = + check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in + let mtb1 = + {typ_mp=mp; + typ_expr=sign; + typ_expr_alg=None; + typ_constraints=Univ.Constraint.empty; + typ_delta = mb.mod_delta;} + and mtb2 = + {typ_mp=mp; + typ_expr=mb.mod_type; + typ_expr_alg=None; + typ_constraints=Univ.Constraint.empty; + typ_delta = mb.mod_delta;}; + in + let env = add_module (module_body_of_type mp mtb1) env in + check_subtypes env mtb1 mtb2 + and check_structure_field env mp lab res = function | SFBconst cb -> let c = make_con mp empty_dirpath lab in @@ -271,7 +280,7 @@ and check_structure_field env mp lab res = function 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 + let (_:unit) = check_module env (MPdot(mp,lab)) msb in Modops.add_module msb env | SFBmodtype mty -> check_module_type env mty; @@ -280,7 +289,7 @@ and check_structure_field env mp lab res = function 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 + (subst_and_strengthen mb mp_mse).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 @@ -293,7 +302,7 @@ and check_modexpr env mse mp_mse res = match mse with try (path_of_mexpr m) with Not_path -> error_application_to_not_path m (* place for nondep_supertype *) in - let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in + let mtb = module_type_of_module (Some mp) (lookup_module mp env) in check_subtypes env mtb farg_b; (subst_struct_expr (map_mbid farg_id mp) fbody_b) | SEBwith(mte, with_decl) -> @@ -301,7 +310,7 @@ and check_modexpr env mse mp_mse res = match mse with let sign = check_with env sign with_decl mp_mse in sign | SEBstruct(msb) -> - let _ = List.fold_left (fun env (lab,mb) -> + let (_:env) = List.fold_left (fun env (lab,mb) -> check_structure_field env mp_mse lab res mb) env msb in SEBstruct(msb) @@ -321,7 +330,7 @@ and check_modtype env mse mp_mse res = match mse with try (path_of_mexpr m) with Not_path -> error_application_to_not_path m (* place for nondep_supertype *) in - let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in + let mtb = module_type_of_module (Some mp) (lookup_module mp env) in check_subtypes env mtb farg_b; subst_struct_expr (map_mbid farg_id mp) fbody_b | SEBwith(mte, with_decl) -> @@ -329,7 +338,7 @@ and check_modtype env mse mp_mse res = match mse with let sign = check_with env sign with_decl mp_mse in sign | SEBstruct(msb) -> - let _ = List.fold_left (fun env (lab,mb) -> + let (_:env) = List.fold_left (fun env (lab,mb) -> 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 6d53803b..38aeaee2 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* anomaly "Modops:the evaluation of the structure failed " -let strengthen_const env mp_from l cb resolver = +let strengthen_const mp_from l cb resolver = match cb.const_opaque, cb.const_body with | false, Some _ -> cb | true, Some _ @@ -126,14 +126,14 @@ let strengthen_const env mp_from l cb resolver = } -let rec strengthen_mod env mp_from mp_to mb = +let rec strengthen_mod mp_from mp_to mb = if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb else match mb.mod_type with | SEBstruct (sign) -> let resolve_out,sign_out = - strengthen_sig env mp_from sign mp_to mb.mod_delta in + strengthen_sig mp_from sign mp_to mb.mod_delta in { mb with mod_expr = Some (SEBident mp_to); mod_type = SEBstruct(sign_out); @@ -145,60 +145,49 @@ let rec strengthen_mod env mp_from mp_to mb = | SEBfunctor _ -> mb | _ -> anomaly "Modops:the evaluation of the structure failed " -and strengthen_sig env mp_from sign mp_to resolver = +and strengthen_sig mp_from sign mp_to resolver = match sign with | [] -> empty_delta_resolver,[] | (l,SFBconst cb) :: rest -> - let item' = - l,SFBconst (strengthen_const env mp_from l cb resolver) in - let resolve_out,rest' = - strengthen_sig env mp_from rest mp_to resolver in - resolve_out,item'::rest' + let item' = l,SFBconst (strengthen_const mp_from l cb resolver) in + let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in + resolve_out,item'::rest' | (_,SFBmind _ as item):: rest -> - let resolve_out,rest' = - strengthen_sig env mp_from rest mp_to resolver in - resolve_out,item::rest' + let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in + resolve_out,item::rest' | (l,SFBmodule mb) :: rest -> let mp_from' = MPdot (mp_from,l) in - let mp_to' = MPdot(mp_to,l) in - let mb_out = - strengthen_mod env mp_from' mp_to' mb in + let mp_to' = MPdot(mp_to,l) in + let mb_out = strengthen_mod mp_from' mp_to' mb in let item' = l,SFBmodule (mb_out) in - let env' = add_module mb_out env in - let resolve_out,rest' = - strengthen_sig env' mp_from rest mp_to resolver in - resolve_out - (*add_delta_resolver resolve_out mb.mod_delta*), - item':: rest' - | (l,SFBmodtype mty as item) :: rest -> - let env' = add_modtype - (MPdot(mp_from,l)) mty env - in - let resolve_out,rest' = - strengthen_sig env' mp_from rest mp_to resolver in - resolve_out,item::rest' - -let strengthen env mtb mp = + let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in + resolve_out, item'::rest' + | (l,SFBmodtype mty as item) :: rest -> + let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in + resolve_out, item::rest' + +let strengthen mtb mp = match mtb.typ_expr with - | SEBstruct (sign) -> + | SEBstruct (sign) -> let resolve_out,sign_out = - strengthen_sig env mtb.typ_mp sign mp mtb.typ_delta in - {mtb with - typ_expr = SEBstruct(sign_out); - typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta + strengthen_sig mtb.typ_mp sign mp mtb.typ_delta + in + {mtb with + typ_expr = SEBstruct(sign_out); + typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta (add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)} | SEBfunctor _ -> mtb | _ -> anomaly "Modops:the evaluation of the structure failed " -let subst_and_strengthen mb mp env = - strengthen_mod env mb.mod_mp mp +let subst_and_strengthen mb mp = + strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb) -let module_type_of_module env mp mb = +let module_type_of_module mp mb = match mp with Some mp -> - strengthen env { + strengthen { typ_mp = mp; typ_expr = mb.mod_type; typ_expr_alg = None; diff --git a/checker/modops.mli b/checker/modops.mli index b218b052..2f9f2e8c 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* module_type_body -> module_body -val module_type_of_module : env -> module_path option -> module_body -> +val module_type_of_module : module_path option -> module_body -> module_type_body val destr_functor : @@ -35,9 +35,9 @@ val add_module : module_body -> env -> env val check_modpath_equiv : env -> module_path -> module_path -> unit -val strengthen : env -> module_type_body -> module_path -> module_type_body +val strengthen : module_type_body -> module_path -> module_type_body -val subst_and_strengthen : module_body -> module_path -> env -> module_body +val subst_and_strengthen : module_body -> module_path -> module_body val error_incompatible_modtypes : module_type_body -> module_type_body -> 'a diff --git a/checker/reduction.ml b/checker/reduction.ml index d040c3db..ba8ceeef 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* error () let rec check_modules env msb1 msb2 subst1 subst2 = - let mty1 = module_type_of_module env None msb1 in - let mty2 = module_type_of_module env None msb2 in + let mty1 = module_type_of_module None msb1 in + let mty2 = module_type_of_module None msb2 in check_modtypes env mty1 mty2 subst1 subst2 false; @@ -343,7 +343,8 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = (module_body_of_type (MPbound arg_id2) arg_t2) env in let env = match body_t1 with - SEBstruct str -> + SEBstruct str -> + let env = shallow_remove_module mtb1.typ_mp env in add_module {mod_mp = mtb1.typ_mp; mod_expr = None; mod_type = body_t1; @@ -363,10 +364,8 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = let check_subtypes env sup super = (*if sup<>super then*) - 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 + check_modtypes env (strengthen 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/subtyping.mli b/checker/subtyping.mli index d88ee0b2..d9cbe5ad 100644 --- a/checker/subtyping.mli +++ b/checker/subtyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* module_type_body -> module_type_body -> unit val check_equal : env -> module_type_body -> module_type_body -> unit diff --git a/checker/term.ml b/checker/term.ml index f472f994..61369586 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*