From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- checker/safe_typing.ml | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) (limited to 'checker/safe_typing.ml') diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index f4ffb302..8f5d4573 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -30,9 +30,8 @@ let set_engagement c = (* full_add_module adds module with universes and constraints *) let full_add_module dp mb digest = let env = !genv in - let mp = MPfile dp in let env = add_constraints mb.mod_constraints env in - let env = Modops.add_module mp mb env in + let env = Modops.add_module mb env in genv := add_digest env dp digest (* Check that the engagement expected by a library matches the initial one *) @@ -58,7 +57,7 @@ let check_imports f caller env needed = try let actual_stamp = lookup_digest env dp in if stamp <> actual_stamp then report_clash f caller dp - with Not_found -> + with Not_found -> error ("Reference to unknown module " ^ (string_of_dirpath dp)) in List.iter check needed @@ -66,46 +65,46 @@ let check_imports f caller env needed = (* Remove the body of opaque constants in modules *) -(* also remove mod_expr ? *) +(* also remove mod_expr ? Good idea!*) let rec lighten_module mb = { mb with mod_expr = Option.map lighten_modexpr mb.mod_expr; - mod_type = Option.map lighten_modexpr mb.mod_type } + mod_type = lighten_modexpr mb.mod_type } -and lighten_struct struc = +and lighten_struct struc = let lighten_body (l,body) = (l,match body with | SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None} - | (SFBconst _ | SFBmind _ | SFBalias _) as x -> x + | (SFBconst _ | SFBmind _ ) as x -> x | SFBmodule m -> SFBmodule (lighten_module m) - | SFBmodtype m -> SFBmodtype - ({m with + | SFBmodtype m -> SFBmodtype + ({m with typ_expr = lighten_modexpr m.typ_expr})) in List.map lighten_body struc and lighten_modexpr = function | SEBfunctor (mbid,mty,mexpr) -> - SEBfunctor (mbid, - ({mty with + SEBfunctor (mbid, + ({mty with typ_expr = lighten_modexpr mty.typ_expr}), lighten_modexpr mexpr) | SEBident mp as x -> x - | SEBstruct (msid, struc) -> - SEBstruct (msid, lighten_struct struc) + | SEBstruct ( struc) -> + SEBstruct ( lighten_struct struc) | SEBapply (mexpr,marg,u) -> SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u) | SEBwith (seb,wdcl) -> - SEBwith (lighten_modexpr seb,wdcl) - + SEBwith (lighten_modexpr seb,wdcl) + let lighten_library (dp,mb,depends,s) = (dp,lighten_module mb,depends,s) -type compiled_library = +type compiled_library = dir_path * module_body * (dir_path * Digest.t) list * engagement option - + open Validate let val_deps = val_list (val_tuple"dep"[|val_dp;no_val|]) let val_vo = val_tuple "vo" [|val_dp;val_module;val_deps;val_opt val_eng|] @@ -119,20 +118,21 @@ let stamp_library file digest = () (* When the module is checked, digests do not need to match, but a warning is issued in case of mismatch *) -let import file (dp,mb,depends,engmt as vo) digest = +let import file (dp,mb,depends,engmt as vo) digest = Validate.apply !Flags.debug val_vo vo; Flags.if_verbose msgnl (str "*** vo structure validated ***"); let env = !genv in check_imports msg_warning dp env depends; check_engagement env engmt; - check_module (add_constraints mb.mod_constraints env) mb; + check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb; stamp_library file digest; (* We drop proofs once checked *) (* let mb = lighten_module mb in*) full_add_module dp mb digest (* When the module is admitted, digests *must* match *) -let unsafe_import file (dp,mb,depends,engmt) digest = +let unsafe_import file (dp,mb,depends,engmt as vo) digest = +(* if !Flags.debug then Validate.apply !Flags.debug val_vo vo;*) let env = !genv in check_imports (errorlabstrm"unsafe_import") dp env depends; check_engagement env engmt; -- cgit v1.2.3