diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 196 |
1 files changed, 98 insertions, 98 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 97697f5de6..3f38cc2f7c 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -22,7 +22,7 @@ open Mod_subst -let error_existing_label l = +let error_existing_label l = error ("The label "^string_of_label l^" is already declared.") let error_declaration_not_path _ = error "Declaration is not a path." @@ -39,31 +39,31 @@ let error_not_match l _ = error ("Signature components for label "^string_of_lab let error_no_such_label l = error ("No such label "^string_of_label l^".") -let error_incompatible_labels l l' = +let error_incompatible_labels l l' = error ("Opening and closing labels are not the same: " ^string_of_label l^" <> "^string_of_label l'^" !") -let error_result_must_be_signature () = +let error_result_must_be_signature () = error "The result module type must be a signature." let error_signature_expected mtb = error "Signature expected." -let error_no_module_to_end _ = +let error_no_module_to_end _ = error "No open module to end." let error_no_modtype_to_end _ = error "No open module type to end." -let error_not_a_modtype_loc loc s = +let error_not_a_modtype_loc loc s = user_err_loc (loc,"",str ("\""^s^"\" is not a module type.")) -let error_not_a_module_loc loc s = +let error_not_a_module_loc loc s = user_err_loc (loc,"",str ("\""^s^"\" is not a module.")) let error_not_a_module s = error_not_a_module_loc dummy_loc s -let error_not_a_constant l = +let error_not_a_constant l = error ("\""^(string_of_label l)^"\" is not a constant.") let error_with_incorrect l = @@ -74,9 +74,9 @@ let error_a_generative_module_expected l = "component of generative modules can be changed using the \"with\" " ^ "construct.") -let error_local_context lo = +let error_local_context lo = match lo with - None -> + None -> error ("The local context is not empty.") | (Some l) -> error ("The local context of the component "^ @@ -106,7 +106,7 @@ let destr_functor env mtb = (* the constraints are not important here *) -let module_body_of_type mtb = +let module_body_of_type mtb = { mod_type = Some mtb.typ_expr; mod_expr = None; mod_constraints = Constraint.empty; @@ -114,30 +114,30 @@ let module_body_of_type mtb = mod_retroknowledge = []} let module_type_of_module mp mb = - let mp1,expr = + let mp1,expr = (match mb.mod_type with | Some expr -> mp,expr | None -> (match mb.mod_expr with | Some (SEBident mp') ->(Some mp'),(SEBident mp') | Some expr -> mp,expr - | None -> + | None -> anomaly "Modops: empty expr and type")) in {typ_expr = expr; typ_alias = mb.mod_alias; typ_strength = mp1 } -let rec check_modpath_equiv env mp1 mp2 = +let rec check_modpath_equiv env mp1 mp2 = if mp1=mp2 then () else let mp1 = scrape_alias mp1 env in let mp2 = scrape_alias mp2 env in if mp1=mp2 then () - else + else error_not_equal mp1 mp2 - + let rec subst_with_body sub = function | With_module_body(id,mp,typ_opt,cst) -> - With_module_body(id,subst_mp sub mp,Option.smartmap + With_module_body(id,subst_mp sub mp,Option.smartmap (subst_struct_expr sub) typ_opt,cst) | With_definition_body(id,cb) -> With_definition_body( id,subst_const_body sub cb) @@ -148,22 +148,22 @@ and subst_modtype sub mtb = if typ_expr'==mtb.typ_expr && sub_mtb==mtb.typ_alias then mtb else - { mtb with + { mtb with typ_expr = typ_expr'; typ_alias = sub_mtb} - -and subst_structure sub sign = + +and subst_structure sub sign = let subst_body = function - SFBconst cb -> + SFBconst cb -> SFBconst (subst_const_body sub cb) - | SFBmind mib -> + | SFBmind mib -> SFBmind (subst_mind sub mib) - | SFBmodule mb -> + | SFBmodule mb -> SFBmodule (subst_module sub mb) - | SFBmodtype mtb -> + | SFBmodtype mtb -> SFBmodtype (subst_modtype sub mtb) | SFBalias (mp,typ_opt,cst) -> - SFBalias (subst_mp sub mp,Option.smartmap + SFBalias (subst_mp sub mp,Option.smartmap (subst_struct_expr sub) typ_opt,cst) in List.map (fun (l,b) -> (l,subst_body b)) sign @@ -177,15 +177,15 @@ and subst_module sub mb = let me' = Option.smartmap (subst_struct_expr sub) mb.mod_expr in let mb_alias = update_subst sub mb.mod_alias in let mb_alias = if mb_alias = empty_subst then - join_alias mb.mod_alias sub - else + join_alias mb.mod_alias sub + else join mb_alias (join_alias mb.mod_alias sub) in - if mtb'==mb.mod_type && mb.mod_expr == me' + if mtb'==mb.mod_type && mb.mod_expr == me' && mb_alias == mb.mod_alias then mb else { mod_expr = me'; - mod_type=mtb'; + mod_type=mtb'; mod_constraints=mb.mod_constraints; mod_alias = mb_alias; mod_retroknowledge=mb.mod_retroknowledge} @@ -193,7 +193,7 @@ and subst_module sub mb = and subst_struct_expr sub = function | SEBident mp -> SEBident (subst_mp sub mp) - | SEBfunctor (msid, mtb, meb') -> + | SEBfunctor (msid, mtb, meb') -> SEBfunctor(msid,subst_modtype sub mtb,subst_struct_expr sub meb') | SEBstruct (msid,str)-> SEBstruct(msid, subst_structure sub str) @@ -201,15 +201,15 @@ and subst_struct_expr sub = function SEBapply(subst_struct_expr sub meb1, subst_struct_expr sub meb2, cst) - | SEBwith (meb,wdb)-> + | SEBwith (meb,wdb)-> SEBwith(subst_struct_expr sub meb, subst_with_body sub wdb) - -let subst_signature_msid msid mp = + +let subst_signature_msid msid mp = subst_structure (map_msid msid mp) -(* spiwack: here comes the function which takes care of importing +(* spiwack: here comes the function which takes care of importing the retroknowledge declared in the library *) (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) let add_retroknowledge msid mp = @@ -217,8 +217,8 @@ let add_retroknowledge msid mp = let subst_and_perform rkaction env = match rkaction with | Retroknowledge.RKRegister (f, e) -> - Environ.register env f - (match e with + Environ.register env f + (match e with | Const kn -> kind_of_term (subst_mps subst (mkConst kn)) | Ind ind -> kind_of_term (subst_mps subst (mkInd ind)) | _ -> anomaly "Modops.add_retroknowledge: had to import an unsupported kind of term") @@ -229,41 +229,41 @@ let add_retroknowledge msid mp = int31 type registration absolutely needs int31 bits to be registered. Since the local_retroknowledge is stored in reverse order (each new registration is added at the top of the list) we need a fold_right - for things to go right (the pun is not intented). So we lose + for things to go right (the pun is not intented). So we lose tail recursivity, but the world will have exploded before any module imports 10 000 retroknowledge registration.*) List.fold_right subst_and_perform lclrk env -let strengthen_const env mp l cb = +let strengthen_const env mp l cb = match cb.const_opaque, cb.const_body with | false, Some _ -> cb - | true, Some _ + | true, Some _ | _, None -> - let const = mkConst (make_con mp empty_dirpath l) in + let const = mkConst (make_con mp empty_dirpath l) in let const_subs = Some (Declarations.from_val const) in - {cb with + {cb with const_body = const_subs; const_opaque = false; const_body_code = Cemitcodes.from_val (compile_constant_body env const_subs false false) } - + let strengthen_mind env mp l mib = match mib.mind_equiv with | Some _ -> mib | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)} -let rec eval_struct env = function - | SEBident mp -> +let rec eval_struct env = function + | SEBident mp -> begin let mtb =lookup_modtype mp env in match mtb.typ_expr,mtb.typ_strength with mtb,None -> eval_struct env mtb | mtb,Some mp -> strengthen_mtb env mp (eval_struct env mtb) end - | SEBapply (seb1,seb2,_) -> + | SEBapply (seb1,seb2,_) -> let svb1 = eval_struct env seb1 in let farg_id, farg_b, fbody_b = destr_functor env svb1 in let mp = path_of_seb seb2 in @@ -271,15 +271,15 @@ let rec eval_struct env = function let sub_alias = (lookup_modtype mp env).typ_alias in let sub_alias = match eval_struct env (SEBident mp) with | SEBstruct (msid,sign) -> - join_alias + join_alias (subst_key (map_msid msid mp) sub_alias) (map_msid msid mp) | _ -> sub_alias in let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in - let sub_alias1 = update_subst sub_alias + let sub_alias1 = update_subst sub_alias (map_mbid farg_id mp (Some resolve)) in - eval_struct env (subst_struct_expr - (join sub_alias1 + eval_struct env (subst_struct_expr + (join sub_alias1 (map_mbid farg_id mp (Some resolve))) fbody_b) | SEBwith (mtb,(With_definition_body _ as wdb)) -> let mtb',_ = merge_with env mtb wdb empty_subst in @@ -292,24 +292,24 @@ let rec eval_struct env = function | _ -> alias_in_mp in let mtb',_ = merge_with env mtb wdb alias_in_mp in mtb' -(* | SEBfunctor(mbid,mtb,body) -> +(* | SEBfunctor(mbid,mtb,body) -> let env = add_module (MPbound mbid) (module_body_of_type mtb) env in SEBfunctor(mbid,mtb,eval_struct env body) *) | mtb -> mtb - + and type_of_mb env mb = match mb.mod_type,mb.mod_expr with None,Some b -> eval_struct env b | Some t, _ -> eval_struct env t - | _,_ -> anomaly - "Modops: empty type and empty expr" - -and merge_with env mtb with_decl alias= - let msid,sig_b = match (eval_struct env mtb) with + | _,_ -> anomaly + "Modops: empty type and empty expr" + +and merge_with env mtb with_decl alias= + let msid,sig_b = match (eval_struct env mtb) with | SEBstruct(msid,sig_b) -> msid,sig_b | _ -> error_signature_expected mtb in - let id,idl = match with_decl with + let id,idl = match with_decl with | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) -> id,idl | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false in @@ -320,20 +320,20 @@ and merge_with env mtb with_decl alias= let rec mp_rec = function | [] -> MPself msid | i::r -> MPdot(mp_rec r,label_of_id i) - in + in let env' = add_signature (MPself msid) before env in let new_spec,subst = match with_decl with | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false - | With_definition_body ([id],c) -> + | With_definition_body ([id],c) -> SFBconst c,None | With_module_body ([id], mp,typ_opt,cst) -> let mp' = scrape_alias mp env' in let new_alias = update_subst alias (map_mp (mp_rec [id]) mp') in SFBalias (mp,typ_opt,Some cst), Some(join (map_mp (mp_rec [id]) mp') new_alias) - | With_definition_body (_::_,_) - | With_module_body (_::_,_,_,_) -> + | With_definition_body (_::_,_) + | With_module_body (_::_,_,_,_) -> let old,aliasold = match spec with SFBmodule msb -> Some msb, None | SFBalias (mpold,typ_opt,cst) ->None, Some (mpold,typ_opt,cst) @@ -341,24 +341,24 @@ and merge_with env mtb with_decl alias= in if aliasold = None then let old = Option.get old in - let new_with_decl,subst1 = + let new_with_decl,subst1 = match with_decl with With_definition_body (_,c) -> With_definition_body (idl,c),None - | With_module_body (idc,mp,typ_opt,cst) -> + | With_module_body (idc,mp,typ_opt,cst) -> let mp' = scrape_alias mp env' in With_module_body (idl,mp,typ_opt,cst), - Some(map_mp (mp_rec (List.rev idc)) mp') + Some(map_mp (mp_rec (List.rev idc)) mp') in let subst = match subst1 with | None -> None | Some s -> Some (join s (update_subst alias s)) in - let modtype,subst_msb = + let modtype,subst_msb = merge_with env' (type_of_mb env' old) new_with_decl alias in let msb = { mod_expr = None; - mod_type = Some modtype; + mod_type = Some modtype; mod_constraints = old.mod_constraints; - mod_alias = begin + mod_alias = begin match subst_msb with |None -> empty_subst |Some s -> s @@ -366,8 +366,8 @@ and merge_with env mtb with_decl alias= mod_retroknowledge = old.mod_retroknowledge} in (SFBmodule msb),subst - else - let mpold,typ_opt,cst = Option.get aliasold in + else + let mpold,typ_opt,cst = Option.get aliasold in SFBalias (mpold,typ_opt,cst),None in SEBstruct(msid, before@(l,new_spec):: @@ -375,36 +375,36 @@ and merge_with env mtb with_decl alias= with Not_found -> error_no_such_label l -and add_signature mp sign env = +and add_signature mp sign env = let add_one env (l,elem) = let kn = make_kn mp empty_dirpath l in let con = make_con mp empty_dirpath l in match elem with | SFBconst cb -> Environ.add_constant con cb env | SFBmind mib -> Environ.add_mind kn mib env - | SFBmodule mb -> - add_module (MPdot (mp,l)) mb env + | SFBmodule mb -> + add_module (MPdot (mp,l)) mb env (* adds components as well *) - | SFBalias (mp1,_,cst) -> + | SFBalias (mp1,_,cst) -> Environ.register_alias (MPdot(mp,l)) mp1 env - | SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l)) + | SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l)) mtb env in List.fold_left add_one env sign -and add_module mp mb env = +and add_module mp mb env = let env = Environ.shallow_add_module mp mb env in let env = Environ.add_modtype mp (module_type_of_module (Some mp) mb) env in let mod_typ = type_of_mb env mb in match mod_typ with - | SEBstruct (msid,sign) -> + | SEBstruct (msid,sign) -> add_retroknowledge msid mp (mb.mod_retroknowledge) (add_signature mp (subst_signature_msid msid mp sign) env) | SEBfunctor _ -> env | _ -> anomaly "Modops:the evaluation of the structure failed " - + and constants_of_specification env mp sign = @@ -413,30 +413,30 @@ and constants_of_specification env mp sign = | SFBconst cb -> env,((make_con mp empty_dirpath l),cb)::res | SFBmind _ -> env,res | SFBmodule mb -> - let new_env = add_module (MPdot (mp,l)) mb env in + let new_env = add_module (MPdot (mp,l)) mb env in new_env,(constants_of_modtype env (MPdot (mp,l)) (type_of_mb env mb)) @ res | SFBalias (mp1,typ_opt,cst) -> - let new_env = register_alias (MPdot (mp,l)) mp1 env in + let new_env = register_alias (MPdot (mp,l)) mp1 env in new_env,(constants_of_modtype env (MPdot (mp,l)) (eval_struct env (SEBident mp1))) @ res - | SFBmodtype mtb -> - (* module type dans un module type. - Il faut au moins mettre mtb dans l'environnement (avec le bon - kn pour pouvoir continuer aller deplier les modules utilisant ce + | SFBmodtype mtb -> + (* module type dans un module type. + Il faut au moins mettre mtb dans l'environnement (avec le bon + kn pour pouvoir continuer aller deplier les modules utilisant ce mtb - ex: - Module Type T1. + ex: + Module Type T1. Module Type T2. .... End T2. ..... Declare Module M : T2. - End T2 - si on ne rajoute pas T2 dans l'environement de typage + End T2 + si on ne rajoute pas T2 dans l'environement de typage on va exploser au moment du Declare Module *) - let new_env = Environ.add_modtype (MPdot(mp,l)) mtb env in + let new_env = Environ.add_modtype (MPdot(mp,l)) mtb env in new_env, (constants_of_modtype env (MPdot(mp,l)) mtb.typ_expr) @ res in snd (List.fold_left aux (env,[]) sign) @@ -474,23 +474,23 @@ and resolver_of_environment mbid modtype mp alias env = let resolve = make_resolve constants in Mod_subst.make_resolver resolve - + and strengthen_mtb env mp mtb = - let mtb1 = eval_struct env mtb in + let mtb1 = eval_struct env mtb in match mtb1 with | SEBfunctor _ -> mtb1 - | SEBstruct (msid,sign) -> + | SEBstruct (msid,sign) -> SEBstruct (msid,strengthen_sig env msid sign mp) | _ -> anomaly "Modops:the evaluation of the structure failed " -and strengthen_mod env mp mb = +and strengthen_mod env mp mb = let mod_typ = type_of_mb env mb in { mod_expr = mb.mod_expr; mod_type = Some (strengthen_mtb env mp mod_typ); mod_constraints = mb.mod_constraints; mod_alias = mb.mod_alias; mod_retroknowledge = mb.mod_retroknowledge} - + and strengthen_sig env msid sign mp = match sign with | [] -> [] | (l,SFBconst cb) :: rest -> @@ -504,7 +504,7 @@ and strengthen_sig env msid sign mp = match sign with | (l,SFBmodule mb) :: rest -> let mp' = MPdot (mp,l) in let item' = l,SFBmodule (strengthen_mod env mp' mb) in - let env' = add_module + let env' = add_module (MPdot (MPself msid,l)) mb env in let rest' = strengthen_sig env' msid rest mp in item':: rest' @@ -512,22 +512,22 @@ and strengthen_sig env msid sign mp = match sign with let env' = register_alias (MPdot(MPself msid,l)) mp1 env in let rest' = strengthen_sig env' msid rest mp in item::rest' - | (l,SFBmodtype mty as item) :: rest -> - let env' = add_modtype - (MPdot((MPself msid),l)) + | (l,SFBmodtype mty as item) :: rest -> + let env' = add_modtype + (MPdot((MPself msid),l)) mty env in let rest' = strengthen_sig env' msid rest mp in item::rest' - + let strengthen env mtb mp = strengthen_mtb env mp mtb let update_subst env mb mp = match type_of_mb env mb with - | SEBstruct(msid,str) -> false, join_alias + | SEBstruct(msid,str) -> false, join_alias (subst_key (map_msid msid mp) mb.mod_alias) (map_msid msid mp) | _ -> true, mb.mod_alias |