diff options
Diffstat (limited to 'checker/modops.ml')
| -rw-r--r-- | checker/modops.ml | 61 |
1 files changed, 18 insertions, 43 deletions
diff --git a/checker/modops.ml b/checker/modops.ml index 38aeaee2..2dc5d062 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modops.ml 9872 2007-05-30 16:01:18Z soubiran $ i*) - (*i*) open Util open Pp @@ -25,8 +23,6 @@ let error_not_a_functor _ = error "Application of not a functor" let error_incompatible_modtypes _ _ = error "Incompatible module types" -let error_not_equal _ _ = error "Not equal modules" - let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match") @@ -61,11 +57,6 @@ let destr_functor env mtb = (arg_id,arg_t,body_t) | _ -> error_not_a_functor mtb - -let is_functor = function - | SEBfunctor (arg_id,arg_t,body_t) -> true - | _ -> false - let module_body_of_type mp mtb = { mod_mp = mp; mod_type = mtb.typ_expr; @@ -75,14 +66,6 @@ let module_body_of_type mp mtb = mod_delta = mtb.typ_delta; mod_retroknowledge = []} -let check_modpath_equiv env mp1 mp2 = - if mp1=mp2 then () else - (* let mb1=lookup_module mp1 env in - let mb2=lookup_module mp2 env in - if (delta_of_mp mb1.mod_delta mp1)=(delta_of_mp mb2.mod_delta mp2) - then () - else*) error_not_equal mp1 mp2 - let rec add_signature mp sign resolver env = let add_one env (l,elem) = let kn = make_kn mp empty_dirpath l in @@ -112,23 +95,16 @@ and add_module mb env = let strengthen_const mp_from l cb resolver = - match cb.const_opaque, cb.const_body with - | false, Some _ -> cb - | true, Some _ - | _, None -> + match cb.const_body with + | Def _ -> cb + | _ -> let con = make_con mp_from empty_dirpath l in - (* let con = constant_of_delta resolver con in*) - let const = Const con in - let const_subs = Some (Declarations.from_val const) in - {cb with - const_body = const_subs; - const_opaque = false; - } - + (* let con = constant_of_delta resolver con in*) + { cb with const_body = Def (Declarations.from_val (Const con)) } let rec strengthen_mod mp_from mp_to mb = if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then - mb + mb else match mb.mod_type with | SEBstruct (sign) -> @@ -154,34 +130,33 @@ and strengthen_sig mp_from sign mp_to resolver = resolve_out,item'::rest' | (_,SFBmind _ as item):: rest -> let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in - resolve_out,item::rest' + 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 mp_from' mp_to' mb in let item' = l,SFBmodule (mb_out) in let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in - resolve_out, item'::rest' - | (l,SFBmodtype mty as item) :: rest -> + resolve_out (*add_delta_resolver resolve_out mb.mod_delta*), + 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' + resolve_out,item::rest' let strengthen mtb mp = match mtb.typ_expr with - | SEBstruct (sign) -> + | SEBstruct (sign) -> let resolve_out,sign_out = - 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 + 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 = - strengthen_mod mb.mod_mp mp - (subst_module (map_mp mb.mod_mp mp) mb) + strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb) let module_type_of_module mp mb = |