diff options
Diffstat (limited to 'checker/modops.ml')
| -rw-r--r-- | checker/modops.ml | 405 |
1 files changed, 135 insertions, 270 deletions
diff --git a/checker/modops.ml b/checker/modops.ml index 498bd775..458c84d8 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -18,7 +18,7 @@ open Declarations open Environ (*i*) -let error_not_a_constant l = +let error_not_a_constant l = error ("\""^(string_of_label l)^"\" is not a constant") let error_not_a_functor _ = error "Application of not a functor" @@ -32,13 +32,12 @@ let error_not_match l _ = let error_no_such_label l = error ("No such label "^string_of_label l) -let error_no_such_label_sub l l1 l2 = - let l1 = string_of_msid l1 in - let l2 = string_of_msid l2 in - error (l1^" is not a subtype of "^l2^".\nThe field "^ - string_of_label l^" is missing (or invisible) in "^l1^".") +let error_no_such_label_sub l l1 = + let l1 = string_of_mp l1 in + error ("The field "^ + string_of_label l^" is missing in "^l1^".") -let error_not_a_module_loc loc s = +let error_not_a_module_loc loc s = user_err_loc (loc,"",str ("\""^string_of_label s^"\" is not a module")) let error_not_a_module s = error_not_a_module_loc dummy_loc s @@ -56,38 +55,6 @@ let error_signature_expected mtb = let error_application_to_not_path _ = error "Application to not path" - -let module_body_of_type mtb = - { mod_type = Some mtb.typ_expr; - mod_expr = None; - mod_constraints = Constraint.empty; - mod_alias = mtb.typ_alias; - mod_retroknowledge = []} - -let module_type_of_module mp mb = - {typ_expr = - (match mb.mod_type with - | Some expr -> expr - | None -> (match mb.mod_expr with - | Some expr -> expr - | None -> - anomaly "Modops: empty expr and type")); - typ_alias = mb.mod_alias; - typ_strength = mp - } - - - -let rec list_split_assoc k rev_before = function - | [] -> raise Not_found - | (k',b)::after when k=k' -> rev_before,b,after - | h::tail -> list_split_assoc k (h::rev_before) tail - -let path_of_seb = function - | SEBident mp -> mp - | _ -> anomaly "Modops: evaluation failed." - - let destr_functor env mtb = match mtb with | SEBfunctor (arg_id,arg_t,body_t) -> @@ -95,254 +62,152 @@ let destr_functor env mtb = | _ -> error_not_a_functor mtb -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 - error_not_equal mp1 mp2 - - - -let strengthen_const env mp l cb = - match cb.const_opaque, cb.const_body with - | false, Some _ -> cb - | true, Some _ - | _, None -> - let const = Const (make_con mp empty_dirpath l) in - let const_subs = Some (Declarations.from_val const) in - {cb with - const_body = const_subs; - const_opaque = 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 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; + mod_type_alg = mtb.typ_expr_alg; + mod_expr = None; + mod_constraints = mtb.typ_constraints; + mod_delta = mtb.typ_delta; + mod_retroknowledge = []} -let rec eval_struct env = function - | SEBident mp -> - begin - let mp = scrape_alias mp env in - 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,_) -> - 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 - let mp = scrape_alias mp env in - let sub_alias = (lookup_modtype mp env).typ_alias in - let sub_alias = match eval_struct env (SEBident mp) with - | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub_alias - | _ -> sub_alias in - let sub_alias = update_subst_alias sub_alias - (map_mbid farg_id mp) in - eval_struct env (subst_struct_expr - (join sub_alias (map_mbid farg_id mp)) fbody_b) - | SEBwith (mtb,(With_definition_body _ as wdb)) -> - merge_with env mtb wdb empty_subst - | SEBwith (mtb, (With_module_body (_,mp,_,_) as wdb)) -> - let alias_in_mp = - (lookup_modtype mp env).typ_alias in - merge_with env mtb wdb alias_in_mp -(* | 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 - | SEBstruct(msid,sig_b) -> msid,sig_b - | _ -> error_signature_expected mtb - in - 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 - let l = label_of_id id in - try - let rev_before,spec,after = list_split_assoc l [] sig_b in - let before = List.rev rev_before in - let rec mp_rec = function - | [] -> MPself msid - | i::r -> MPdot(mp_rec r,label_of_id i) - in - let new_spec,subst = match with_decl with - | With_definition_body ([],_) - | With_module_body ([],_,_,_) -> assert false - | With_definition_body ([id],c) -> - SFBconst c,None - | With_module_body ([id], mp,typ_opt,cst) -> - let mp' = scrape_alias mp env in - SFBalias (mp,typ_opt,Some cst), - Some(join (map_mp (mp_rec [id]) mp') alias) - | With_definition_body (_::_,_) - | With_module_body (_::_,_,_,_) -> - let old = match spec with - SFBmodule msb -> msb - | _ -> error_not_a_module l - in - let new_with_decl,subst1 = - match with_decl with - With_definition_body (_,c) -> With_definition_body (idl,c),None - | With_module_body (idc,mp,t,cst) -> - With_module_body (idl,mp,t,cst), - Some(map_mp (mp_rec idc) mp) - in - let subst = Option.fold_right join subst1 alias in - let modtype = - merge_with env (type_of_mb env old) new_with_decl alias in - let msb = - { mod_expr = None; - mod_type = Some modtype; - mod_constraints = old.mod_constraints; - mod_alias = subst; - mod_retroknowledge = old.mod_retroknowledge} - in - (SFBmodule msb),Some subst - in - SEBstruct(msid, before@(l,new_spec):: - (Option.fold_right subst_structure subst after)) - with - Not_found -> error_no_such_label l +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 -and add_signature mp sign env = +let rec add_signature mp sign resolver 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 + let con = constant_of_kn kn in + let mind = mind_of_delta resolver (mind_of_kn kn) 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 + | SFBconst cb -> + (* let con = constant_of_delta resolver con in*) + Environ.add_constant con cb env + | SFBmind mib -> + (* let mind = mind_of_delta resolver mind in*) + Environ.add_mind mind mib env + | SFBmodule mb -> add_module mb env (* adds components as well *) - | SFBalias (mp1,_,cst) -> - Environ.register_alias (MPdot(mp,l)) mp1 env - | SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l)) - mtb env + | SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env in List.fold_left add_one env sign -and add_module mp mb env = +and add_module mb env = + let mp = mb.mod_mp in 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) -> - add_signature mp (subst_signature_msid msid mp sign) env + match mb.mod_type with + | SEBstruct (sign) -> + add_signature mp sign mb.mod_delta env | SEBfunctor _ -> env | _ -> anomaly "Modops:the evaluation of the structure failed " - -and constants_of_specification env mp sign = - let aux (env,res) (l,elem) = - match elem with - | 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 - new_env,(constants_of_modtype env (MPdot (mp,l)) - (type_of_mb env mb)) @ res - | SFBalias (mp1,_,cst) -> - 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 - mtb - 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 - on va exploser au moment du Declare Module - *) - 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) +let strengthen_const env mp_from l cb resolver = + match cb.const_opaque, cb.const_body with + | false, Some _ -> cb + | true, Some _ + | _, None -> + 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; + } + -and constants_of_modtype env mp modtype = - match (eval_struct env modtype) with - SEBstruct (msid,sign) -> - constants_of_specification env mp - (subst_signature_msid msid mp sign) - | SEBfunctor _ -> [] - | _ -> anomaly "Modops:the evaluation of the structure failed " +let rec strengthen_mod env 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 + { mb with + mod_expr = Some (SEBident mp_to); + mod_type = SEBstruct(sign_out); + mod_type_alg = mb.mod_type_alg; + mod_constraints = mb.mod_constraints; + mod_delta = resolve_out(*add_mp_delta_resolver mp_from mp_to + (add_delta_resolver mb.mod_delta resolve_out)*); + mod_retroknowledge = mb.mod_retroknowledge} + | SEBfunctor _ -> mb + | _ -> anomaly "Modops:the evaluation of the structure failed " + +and strengthen_sig env 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' + | (_,SFBmind _ as item):: rest -> + let resolve_out,rest' = + strengthen_sig env 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 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' -and strengthen_mtb env mp mtb = - let mtb1 = eval_struct env mtb in - match mtb1 with - | SEBfunctor _ -> mtb1 - | SEBstruct (msid,sign) -> - SEBstruct (msid,strengthen_sig env msid sign mp) - | _ -> anomaly "Modops:the evaluation of the structure failed " +let strengthen env mtb mp = + match mtb.typ_expr with + | 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 + (add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)} + | SEBfunctor _ -> mtb + | _ -> anomaly "Modops:the evaluation of the structure failed " -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 -> - let item' = l,SFBconst (strengthen_const env mp l cb) in - let rest' = strengthen_sig env msid rest mp in - item'::rest' - | (l,SFBmind mib) :: rest -> - let item' = l,SFBmind (strengthen_mind env mp l mib) in - let rest' = strengthen_sig env msid rest mp in - item'::rest' - | (l,SFBmodule mb) :: rest -> - let mp' = MPdot (mp,l) in - let item' = l,SFBmodule (strengthen_mod env mp' mb) in - let env' = add_module - (MPdot (MPself msid,l)) mb env in - let rest' = strengthen_sig env' msid rest mp in - item':: rest' - | ((l,SFBalias (mp1,_,cst)) as item) :: rest -> - 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)) - mty - env - in - let rest' = strengthen_sig env' msid rest mp in - item::rest' +let subst_and_strengthen mb mp env = + strengthen_mod env mb.mod_mp mp + (subst_module (map_mp mb.mod_mp mp) mb) - -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 - (subst_key (map_msid msid mp) mb.mod_alias) - (map_msid msid mp) - | _ -> true, mb.mod_alias +let module_type_of_module env mp mb = + match mp with + Some mp -> + strengthen env { + typ_mp = mp; + typ_expr = mb.mod_type; + typ_expr_alg = None; + typ_constraints = mb.mod_constraints; + typ_delta = mb.mod_delta} mp + + | None -> + {typ_mp = mb.mod_mp; + typ_expr = mb.mod_type; + typ_expr_alg = None; + typ_constraints = mb.mod_constraints; + typ_delta = mb.mod_delta} |