diff options
| -rw-r--r-- | checker/.depend | 166 | ||||
| -rw-r--r-- | checker/Makefile | 26 | ||||
| -rw-r--r-- | checker/check.ml | 10 | ||||
| -rw-r--r-- | checker/checker.ml | 9 | ||||
| -rw-r--r-- | checker/declarations.ml | 42 | ||||
| -rw-r--r-- | checker/declarations.mli | 1 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 41 | ||||
| -rw-r--r-- | checker/modops.ml | 172 | ||||
| -rw-r--r-- | checker/modops.mli | 2 |
9 files changed, 155 insertions, 314 deletions
diff --git a/checker/.depend b/checker/.depend index dade1591b..09ab6bdd1 100644 --- a/checker/.depend +++ b/checker/.depend @@ -1,116 +1,58 @@ -checker.cmo: ../lib/util.cmi ../kernel/univ.cmi type_errors.cmi \ - /usr/lib/ocaml/camlp4/token.cmi ../kernel/term.cmi ../lib/system.cmi \ - /usr/lib/ocaml/camlp4/stdpp.cmi safe_typing.cmi ../lib/pp.cmi \ - ../kernel/names.cmi indtypes.cmi ../lib/flags.cmi declarations.cmi \ - ../config/coq_config.cmi check_stat.cmi check.cmo -checker.cmx: ../lib/util.cmx ../kernel/univ.cmx type_errors.cmx \ - /usr/lib/ocaml/camlp4/token.cmi ../kernel/term.cmx ../lib/system.cmx \ - /usr/lib/ocaml/camlp4/stdpp.cmi safe_typing.cmx ../lib/pp.cmi \ - ../kernel/names.cmx indtypes.cmx ../lib/flags.cmx declarations.cmx \ - ../config/coq_config.cmx check_stat.cmx check.cmx -check.cmo: ../lib/util.cmi ../lib/system.cmi safe_typing.cmi ../lib/pp.cmi \ - ../kernel/names.cmi ../lib/flags.cmi -check.cmx: ../lib/util.cmx ../lib/system.cmx safe_typing.cmx ../lib/pp.cmi \ - ../kernel/names.cmx ../lib/flags.cmx -check_stat.cmo: ../lib/util.cmi ../kernel/term.cmi ../lib/system.cmi \ - safe_typing.cmi ../lib/pp.cmi ../kernel/names.cmi indtypes.cmi \ - ../lib/flags.cmi ../kernel/environ.cmi declarations.cmi check_stat.cmi -check_stat.cmx: ../lib/util.cmx ../kernel/term.cmx ../lib/system.cmx \ - safe_typing.cmx ../lib/pp.cmi ../kernel/names.cmx indtypes.cmx \ - ../lib/flags.cmx ../kernel/environ.cmx declarations.cmx check_stat.cmi -closure.cmo: ../lib/util.cmi ../kernel/term.cmi ../lib/pp.cmi \ - ../kernel/names.cmi ../kernel/esubst.cmi ../kernel/environ.cmi \ - closure.cmi -closure.cmx: ../lib/util.cmx ../kernel/term.cmx ../lib/pp.cmi \ - ../kernel/names.cmx ../kernel/esubst.cmx ../kernel/environ.cmx \ - closure.cmi -closure.cmi: ../kernel/term.cmi ../lib/pp.cmi ../kernel/names.cmi \ - ../kernel/esubst.cmi ../kernel/environ.cmi -declarations.cmo: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \ - ../lib/rtree.cmi ../lib/option.cmi ../kernel/names.cmi declarations.cmi -declarations.cmx: ../lib/util.cmx ../kernel/univ.cmx ../kernel/term.cmx \ - ../lib/rtree.cmx ../lib/option.cmx ../kernel/names.cmx declarations.cmi -declarations.cmi: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \ - ../lib/rtree.cmi ../kernel/names.cmi -environ.cmo: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \ - ../kernel/names.cmi declarations.cmi -environ.cmx: ../lib/util.cmx ../kernel/univ.cmx ../kernel/term.cmx \ - ../kernel/names.cmx declarations.cmx -indtypes.cmo: ../lib/util.cmi ../kernel/univ.cmi typeops.cmi \ - ../kernel/term.cmi ../lib/rtree.cmi reduction.cmi ../lib/pp.cmi \ - ../kernel/names.cmi inductive.cmi ../lib/flags.cmi ../kernel/environ.cmi \ +checker.cmo: type_errors.cmi term.cmo safe_typing.cmi indtypes.cmi \ + declarations.cmi check_stat.cmi check.cmo +checker.cmx: type_errors.cmx term.cmx safe_typing.cmx indtypes.cmx \ + declarations.cmx check_stat.cmx check.cmx +check.cmo: safe_typing.cmi +check.cmx: safe_typing.cmx +check_stat.cmo: term.cmo safe_typing.cmi indtypes.cmi environ.cmo \ + declarations.cmi check_stat.cmi +check_stat.cmx: term.cmx safe_typing.cmx indtypes.cmx environ.cmx \ + declarations.cmx check_stat.cmi +closure.cmo: term.cmo environ.cmo closure.cmi +closure.cmx: term.cmx environ.cmx closure.cmi +closure.cmi: term.cmo environ.cmo +declarations.cmo: term.cmo declarations.cmi +declarations.cmx: term.cmx declarations.cmi +declarations.cmi: term.cmo +environ.cmo: term.cmo declarations.cmi +environ.cmx: term.cmx declarations.cmx +indtypes.cmo: typeops.cmi term.cmo reduction.cmi inductive.cmi environ.cmo \ declarations.cmi indtypes.cmi -indtypes.cmx: ../lib/util.cmx ../kernel/univ.cmx typeops.cmx \ - ../kernel/term.cmx ../lib/rtree.cmx reduction.cmx ../lib/pp.cmi \ - ../kernel/names.cmx inductive.cmx ../lib/flags.cmx ../kernel/environ.cmx \ +indtypes.cmx: typeops.cmx term.cmx reduction.cmx inductive.cmx environ.cmx \ declarations.cmx indtypes.cmi -indtypes.cmi: ../kernel/univ.cmi typeops.cmi ../kernel/term.cmi ../lib/pp.cmi \ - ../kernel/names.cmi ../kernel/environ.cmi declarations.cmi -inductive.cmo: ../lib/util.cmi ../kernel/univ.cmi type_errors.cmi \ - ../kernel/term.cmi ../lib/rtree.cmi reduction.cmi ../kernel/names.cmi \ - ../kernel/environ.cmi declarations.cmi inductive.cmi -inductive.cmx: ../lib/util.cmx ../kernel/univ.cmx type_errors.cmx \ - ../kernel/term.cmx ../lib/rtree.cmx reduction.cmx ../kernel/names.cmx \ - ../kernel/environ.cmx declarations.cmx inductive.cmi -inductive.cmi: ../kernel/univ.cmi ../kernel/term.cmi ../kernel/names.cmi \ - ../kernel/environ.cmi declarations.cmi +indtypes.cmi: typeops.cmi term.cmo environ.cmo declarations.cmi +inductive.cmo: type_errors.cmi term.cmo reduction.cmi environ.cmo \ + declarations.cmi inductive.cmi +inductive.cmx: type_errors.cmx term.cmx reduction.cmx environ.cmx \ + declarations.cmx inductive.cmi +inductive.cmi: term.cmo environ.cmo declarations.cmi main.cmo: checker.cmo main.cmx: checker.cmx -mod_checking.cmo: ../lib/util.cmi ../kernel/univ.cmi typeops.cmi \ - ../kernel/term.cmi subtyping.cmi reduction.cmi ../lib/pp.cmi \ - ../kernel/names.cmi modops.cmi inductive.cmi indtypes.cmi \ - ../lib/flags.cmi ../kernel/environ.cmi declarations.cmi -mod_checking.cmx: ../lib/util.cmx ../kernel/univ.cmx typeops.cmx \ - ../kernel/term.cmx subtyping.cmx reduction.cmx ../lib/pp.cmi \ - ../kernel/names.cmx modops.cmx inductive.cmx indtypes.cmx \ - ../lib/flags.cmx ../kernel/environ.cmx declarations.cmx -modops.cmo: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \ - ../lib/pp.cmi ../lib/option.cmi ../kernel/names.cmi ../kernel/environ.cmi \ - declarations.cmi modops.cmi -modops.cmx: ../lib/util.cmx ../kernel/univ.cmx ../kernel/term.cmx \ - ../lib/pp.cmi ../lib/option.cmx ../kernel/names.cmx ../kernel/environ.cmx \ - declarations.cmx modops.cmi -modops.cmi: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \ - ../kernel/names.cmi ../kernel/environ.cmi declarations.cmi -reduction.cmo: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \ - ../kernel/names.cmi ../kernel/esubst.cmi ../kernel/environ.cmi \ - closure.cmi reduction.cmi -reduction.cmx: ../lib/util.cmx ../kernel/univ.cmx ../kernel/term.cmx \ - ../kernel/names.cmx ../kernel/esubst.cmx ../kernel/environ.cmx \ - closure.cmx reduction.cmi -reduction.cmi: ../kernel/term.cmi ../kernel/environ.cmi -safe_typing.cmo: validate.cmo ../lib/util.cmi ../lib/pp.cmi ../lib/option.cmi \ - ../kernel/names.cmi modops.cmi mod_checking.cmo ../lib/flags.cmi \ - ../kernel/environ.cmi declarations.cmi safe_typing.cmi -safe_typing.cmx: validate.cmx ../lib/util.cmx ../lib/pp.cmi ../lib/option.cmx \ - ../kernel/names.cmx modops.cmx mod_checking.cmx ../lib/flags.cmx \ - ../kernel/environ.cmx declarations.cmx safe_typing.cmi -safe_typing.cmi: ../kernel/term.cmi ../lib/system.cmi ../kernel/names.cmi \ - ../kernel/environ.cmi declarations.cmi -subtyping.cmo: ../lib/util.cmi ../kernel/univ.cmi typeops.cmi \ - ../kernel/term.cmi reduction.cmi ../lib/pp.cmi ../kernel/names.cmi \ - modops.cmi inductive.cmi ../kernel/environ.cmi declarations.cmi \ - subtyping.cmi -subtyping.cmx: ../lib/util.cmx ../kernel/univ.cmx typeops.cmx \ - ../kernel/term.cmx reduction.cmx ../lib/pp.cmi ../kernel/names.cmx \ - modops.cmx inductive.cmx ../kernel/environ.cmx declarations.cmx \ - subtyping.cmi -subtyping.cmi: ../kernel/univ.cmi ../kernel/term.cmi ../kernel/environ.cmi \ - declarations.cmi -term.cmo: ../lib/util.cmi ../kernel/univ.cmi ../lib/pp.cmi ../lib/option.cmi \ - ../kernel/names.cmi ../kernel/esubst.cmi -term.cmx: ../lib/util.cmx ../kernel/univ.cmx ../lib/pp.cmi ../lib/option.cmx \ - ../kernel/names.cmx ../kernel/esubst.cmx -type_errors.cmo: ../kernel/term.cmi ../kernel/names.cmi ../kernel/environ.cmi \ - type_errors.cmi -type_errors.cmx: ../kernel/term.cmx ../kernel/names.cmx ../kernel/environ.cmx \ - type_errors.cmi -type_errors.cmi: ../kernel/term.cmi ../kernel/names.cmi ../kernel/environ.cmi -typeops.cmo: ../lib/util.cmi ../kernel/univ.cmi type_errors.cmi \ - ../kernel/term.cmi reduction.cmi ../kernel/names.cmi inductive.cmi \ - ../kernel/environ.cmi declarations.cmi typeops.cmi -typeops.cmx: ../lib/util.cmx ../kernel/univ.cmx type_errors.cmx \ - ../kernel/term.cmx reduction.cmx ../kernel/names.cmx inductive.cmx \ - ../kernel/environ.cmx declarations.cmx typeops.cmi -typeops.cmi: ../kernel/term.cmi ../kernel/names.cmi ../kernel/environ.cmi \ - declarations.cmi +mod_checking.cmo: typeops.cmi term.cmo subtyping.cmi reduction.cmi modops.cmi \ + inductive.cmi indtypes.cmi environ.cmo declarations.cmi +mod_checking.cmx: typeops.cmx term.cmx subtyping.cmx reduction.cmx modops.cmx \ + inductive.cmx indtypes.cmx environ.cmx declarations.cmx +modops.cmo: term.cmo environ.cmo declarations.cmi modops.cmi +modops.cmx: term.cmx environ.cmx declarations.cmx modops.cmi +modops.cmi: term.cmo environ.cmo declarations.cmi +reduction.cmo: term.cmo environ.cmo closure.cmi reduction.cmi +reduction.cmx: term.cmx environ.cmx closure.cmx reduction.cmi +reduction.cmi: term.cmo environ.cmo +safe_typing.cmo: validate.cmo modops.cmi mod_checking.cmo environ.cmo \ + declarations.cmi safe_typing.cmi +safe_typing.cmx: validate.cmx modops.cmx mod_checking.cmx environ.cmx \ + declarations.cmx safe_typing.cmi +safe_typing.cmi: term.cmo environ.cmo declarations.cmi +subtyping.cmo: typeops.cmi term.cmo reduction.cmi modops.cmi inductive.cmi \ + environ.cmo declarations.cmi subtyping.cmi +subtyping.cmx: typeops.cmx term.cmx reduction.cmx modops.cmx inductive.cmx \ + environ.cmx declarations.cmx subtyping.cmi +subtyping.cmi: term.cmo environ.cmo declarations.cmi +type_errors.cmo: term.cmo environ.cmo type_errors.cmi +type_errors.cmx: term.cmx environ.cmx type_errors.cmi +type_errors.cmi: term.cmo environ.cmo +typeops.cmo: type_errors.cmi term.cmo reduction.cmi inductive.cmi environ.cmo \ + declarations.cmi typeops.cmi +typeops.cmx: type_errors.cmx term.cmx reduction.cmx inductive.cmx environ.cmx \ + declarations.cmx typeops.cmi +typeops.cmi: term.cmo environ.cmo declarations.cmi diff --git a/checker/Makefile b/checker/Makefile index 7567e78ff..2bcc9d365 100644 --- a/checker/Makefile +++ b/checker/Makefile @@ -10,15 +10,7 @@ OPTFLAGS=$(MLDIRS) CHECKERNAME=coqchk BINARIES=../bin/$(CHECKERNAME)$(EXE) ../bin/$(CHECKERNAME).opt$(EXE) - -MCHECKER:=\ - $(COQSRC)/config/coq_config.cmo \ - $(COQSRC)/lib/pp_control.cmo $(COQSRC)/lib/pp.cmo $(COQSRC)/lib/compat.cmo \ - $(COQSRC)/lib/util.cmo $(COQSRC)/lib/option.cmo $(COQSRC)/lib/hashcons.cmo \ - $(COQSRC)/lib/system.cmo $(COQSRC)/lib/flags.cmo \ - $(COQSRC)/lib/predicate.cmo $(COQSRC)/lib/rtree.cmo \ - $(COQSRC)/kernel/names.cmo $(COQSRC)/kernel/univ.cmo \ - $(COQSRC)/kernel/esubst.cmo term.cmo \ +MCHECKERLOCAL :=\ declarations.cmo environ.cmo \ closure.cmo reduction.cmo \ type_errors.cmo \ @@ -29,15 +21,25 @@ validate.cmo \ safe_typing.cmo check.cmo \ check_stat.cmo checker.cmo +MCHECKER:=\ + $(COQSRC)/config/coq_config.cmo \ + $(COQSRC)/lib/pp_control.cmo $(COQSRC)/lib/pp.cmo $(COQSRC)/lib/compat.cmo \ + $(COQSRC)/lib/util.cmo $(COQSRC)/lib/option.cmo $(COQSRC)/lib/hashcons.cmo \ + $(COQSRC)/lib/system.cmo $(COQSRC)/lib/flags.cmo \ + $(COQSRC)/lib/predicate.cmo $(COQSRC)/lib/rtree.cmo \ + $(COQSRC)/kernel/names.cmo $(COQSRC)/kernel/univ.cmo \ + $(COQSRC)/kernel/esubst.cmo term.cmo \ + $(MCHECKERLOCAL) + all: $(BINARIES) byte : ../bin/$(CHECKERNAME)$(EXE) opt : ../bin/$(CHECKERNAME).opt$(EXE) -check.cma: $(MCHECKER) +check.cma: $(MCHECKERLOCAL) ocamlc $(BYTEFLAGS) -a -o $@ $(MCHECKER) -check.cmxa: $(MCHECKER:.cmo=.cmx) +check.cmxa: $(MCHECKERLOCAL:.cmo=.cmx) ocamlopt $(OPTFLAGS) -a -o $@ $(MCHECKER:.cmo=.cmx) ../bin/$(CHECKERNAME)$(EXE): check.cma @@ -78,7 +80,7 @@ stats: depend:: - ocamldep $(MLDIRS) *.ml* > .depend + ocamldep *.ml* > .depend clean:: rm -f *.cm* *.o *.a *~ $(BINARIES) diff --git a/checker/check.ml b/checker/check.ml index 646063519..7169d709f 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -342,10 +342,12 @@ let rec intern_library (dir, f) needed = and intern_mandatory_library (dir,_) needed = intern_library (try_locate_absolute_library dir) needed -let recheck_library ~admit ~check = - let al = List.map (fun q -> fst(try_locate_qualified_library q)) admit in - let admit = List.fold_right library_dep al LibraryMap.empty in - let modl = List.map try_locate_qualified_library check in +let recheck_library ~norec ~admit ~check = + let nrl = List.map (fun q -> fst(try_locate_qualified_library q)) norec in + let al = List.map (fun q -> fst(try_locate_qualified_library q)) admit in + let admit = List.fold_right library_dep (nrl@al) LibraryMap.empty in + let admit = List.fold_right LibraryMap.remove nrl admit in + let modl = List.map try_locate_qualified_library (norec@check) in let needed = List.rev (List.fold_right intern_library modl []) in Flags.if_verbose msgnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++ prlist diff --git a/checker/checker.ml b/checker/checker.ml index 832fe0663..0ae94444d 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -152,6 +152,10 @@ let admit_list = ref ([] : section_path list) let add_admit s = admit_list := path_of_string s :: !admit_list +let norec_list = ref ([] : section_path list) +let add_norec s = + norec_list := path_of_string s :: !norec_list + let compile_list = ref ([] : section_path list) let add_compile s = compile_list := path_of_string s :: !compile_list @@ -162,6 +166,7 @@ let add_compile s = let compile_files () = Check.recheck_library + ~norec:(List.rev !norec_list) ~admit:(List.rev !admit_list) ~check:(List.rev !compile_list) @@ -182,6 +187,7 @@ let print_usage_channel co command = -R dir coqdir recursively map physical dir to logical coqdir -admit module load module and dependencies without checking + -norec module check module but admit dependencies without checking -where print Coq's standard library location and exit -v print Coq version and exit @@ -325,6 +331,9 @@ let parse_args() = | "-admit" :: s :: rem -> add_admit s; parse rem | "-admit" :: [] -> usage () + | "-norec" :: s :: rem -> add_norec s; parse rem + | "-norec" :: [] -> usage () + | "-silent" :: rem -> Flags.make_silent true; parse rem diff --git a/checker/declarations.ml b/checker/declarations.ml index 94388f4ac..71b6c9ca0 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -306,6 +306,48 @@ let join_alias (subst1 : substitution) (subst2 : substitution) = Umap.mapi (apply_subst subst2) subst1 +let update_subst subst1 subst2 = + let subst_inv key (mp,_) l = + let newmp = + match key with + | MBI msid -> MPbound msid + | MSI msid -> MPself msid + | MPI mp -> mp + in + match mp with + | MPbound mbid -> ((MBI mbid),newmp)::l + | MPself msid -> ((MSI msid),newmp)::l + | _ -> ((MPI mp),newmp)::l + in + let subst_mbi = Umap.fold subst_inv subst2 [] in + let alias_subst key (mp,_) sub= + let newsetkey = + match key with + | MPI mp1 -> + let compute_set_newkey l (k,mp') = + let mp_from_key = match k with + | MBI msid -> MPbound msid + | MSI msid -> MPself msid + | MPI mp -> mp + in + let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in + if new_mp1 == mp1 then l else (MPI new_mp1)::l + in + begin + match List.fold_left compute_set_newkey [] subst_mbi with + | [] -> None + | l -> Some (l) + end + | _ -> None + in + match newsetkey with + | None -> sub + | Some l -> + List.fold_left (fun s k -> Umap.add k (mp,None) s) + sub l + in + Umap.fold alias_subst subst1 empty_subst + let subst_substituted s r = match !r with diff --git a/checker/declarations.mli b/checker/declarations.mli index ceb96d635..fdea3383b 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -208,4 +208,5 @@ val subst_signature_msid : val join : substitution -> substitution -> substitution val join_alias : substitution -> substitution -> substitution val update_subst_alias : substitution -> substitution -> substitution +val update_subst : substitution -> substitution -> substitution val subst_key : substitution -> substitution -> substitution diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 9c1cf8ed3..ecf8d6332 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -182,11 +182,6 @@ let check_definition_sub env cb1 cb2 = Reduction.conv env c1 c2 | _ -> ()) -let is_functor env mb = - match type_of_mb env mb with - | SEBstruct(msid,str) -> false - | _ -> true - let rec check_with env mtb with_decl = match with_decl with | With_definition_body _ -> @@ -344,13 +339,16 @@ and check_structure_field (s,env) mp lab = function (s,Indtypes.check_inductive env kn mib) | SFBmodule msb -> check_module env msb; - ((if is_functor env msb then s else join s msb.mod_alias), + let mp1 = MPdot(mp,lab) in + let is_fun, sub = Modops.update_subst env msb mp1 in + ((if is_fun then s else join s sub), Modops.add_module (MPdot(mp,lab)) msb (add_module_constraints env msb)) | SFBalias(mp2,cst) -> (try - let msb = lookup_module mp2 env in - (add_mp (MPdot(mp,lab)) mp2 (join s msb.mod_alias), + let mp2' = scrape_alias mp2 env in + let msb = lookup_module mp2' env in + (join s (add_mp (MPdot(mp,lab)) mp2' msb.mod_alias), Option.fold_right add_constraints cst (register_alias (MPdot(mp,lab)) mp2 env)) with Not_found -> failwith "unkown aliased module") @@ -367,24 +365,27 @@ and check_modexpr env mse = match mse with | SEBfunctor (arg_id, mtb, body) -> check_module_type env mtb; let env' = add_module (MPbound arg_id) (module_body_of_type mtb) env in - check_modexpr env' body + let sub = check_modexpr env' body in + sub | SEBapply (f,m,cst) -> let sub1 = check_modexpr env f in let f'= eval_struct env f in let farg_id, farg_b, fbody_b = destr_functor env f' in - let mtb = - try - lookup_modtype (path_of_mexpr m) env - with - | Not_path -> error_application_to_not_path m + let mp = + try scrape_alias (path_of_mexpr m) env + with Not_path -> error_application_to_not_path m (* place for nondep_supertype *) in - let sub2= check_modexpr env m in - let sub = join sub1 sub2 in - let sub = join_alias sub (map_mbid farg_id (path_of_mexpr m)) in - let sub = - update_subst_alias sub (map_mbid farg_id (path_of_mexpr m)) in + let mtb = lookup_modtype mp env in check_subtypes env mtb farg_b; - sub + let sub2 = match eval_struct env m with + | SEBstruct (msid,sign) -> + join_alias + (subst_key (map_msid msid mp) mtb.typ_alias) + (map_msid msid mp) + | _ -> mtb.typ_alias in + let sub3 = join_alias sub1 (map_mbid farg_id mp) in + let sub4 = update_subst sub2 sub3 in + join sub3 sub4 | SEBwith(mte, with_decl) -> let sub1 = check_modexpr env mte in let sub2 = check_with env mte with_decl in diff --git a/checker/modops.ml b/checker/modops.ml index fc8636a0b..f79e52c2e 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -339,169 +339,9 @@ and strengthen_sig env msid sign mp = match sign with let strengthen env mtb mp = strengthen_mtb env mp mtb - -(* - - -let rec scrape_modtype env = function - | MTBident kn -> - let mtb = - try lookup_modtype kn env - with Not_found -> - anomalylabstrm "scrape_modtype" - (str"scrape_modtype: cannot find "(*++pr_kn kn*)) in - scrape_modtype env mtb - | mtb -> mtb - - -(* the constraints are not important here *) -let module_spec_of_body mb = - { msb_modtype = mb.mod_type; - msb_equiv = mb.mod_equiv; - msb_constraints = Constraint.empty} - - - -let destr_functor = function - | MTBfunsig (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t) - | mtb -> error_not_a_functor mtb - -let rec check_modpath_equiv env mp1 mp2 = - if mp1=mp2 then () else - let mb1 = lookup_module mp1 env in - match mb1.mod_equiv with - | None -> - let mb2 = lookup_module mp2 env in - (match mb2.mod_equiv with - | None -> error_not_equal mp1 mp2 - | Some mp2' -> check_modpath_equiv env mp2' mp1) - | Some mp1' -> check_modpath_equiv env mp2 mp1' - - -(* we assume that the substitution of "mp" into "msid" is already done -(or unnecessary) *) -let rec 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 - | SPBconst cb -> add_constant con cb env - | SPBmind mib -> add_mind kn mib env - | SPBmodule mb -> - add_module (MPdot (mp,l)) (module_body_of_spec mb) env - (* adds components as well *) - | SPBmodtype mtb -> add_modtype kn mtb env - in - List.fold_left add_one env sign - - -and add_module mp mb env = - let env = shallow_add_module mp mb env in - match scrape_modtype env mb.mod_type with - | MTBident _ -> anomaly "scrape_modtype does not work!" - | MTBsig (msid,sign) -> - add_signature mp (subst_signature_msid msid mp sign) env - | MTBfunsig _ -> env - - -let rec constants_of_specification env mp sign = - let aux (env,res) (l,elem) = - match elem with - | SPBconst cb -> env,((make_con mp empty_dirpath l),cb)::res - | SPBmind _ -> env,res - | SPBmodule mb -> - let new_env = add_module (MPdot (mp,l)) (module_body_of_spec mb) env in - new_env,(constants_of_modtype env (MPdot (mp,l)) - (module_body_of_spec mb).mod_type) @ res - | SPBmodtype 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 = add_modtype (make_kn mp empty_dirpath l) mtb env in - new_env, constants_of_modtype env (MPdot(mp,l)) mtb @ res - in - snd (List.fold_left aux (env,[]) sign) - -and constants_of_modtype env mp modtype = - match scrape_modtype env modtype with - MTBident _ -> anomaly "scrape_modtype does not work!" - | MTBsig (msid,sign) -> - constants_of_specification env mp - (subst_signature_msid msid mp sign) - | MTBfunsig _ -> [] - - -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 (from_val const) in - {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 strengthen_mtb env mp mtb = match scrape_modtype env mtb with - | MTBident _ -> anomaly "scrape_modtype does not work!" - | MTBfunsig _ -> mtb - | MTBsig (msid,sign) -> MTBsig (msid,strengthen_sig env msid sign mp) - -and strengthen_mod env mp msb = - { msb_modtype = strengthen_mtb env mp msb.msb_modtype; - msb_equiv = begin match msb.msb_equiv with - | Some _ -> msb.msb_equiv - | None -> Some mp - end ; - msb_constraints = msb.msb_constraints; } - -and strengthen_sig env msid sign mp = match sign with - | [] -> [] - | (l,SPBconst cb) :: rest -> - let item' = l,SPBconst (strengthen_const env mp l cb) in - let rest' = strengthen_sig env msid rest mp in - item'::rest' - | (l,SPBmind mib) :: rest -> - let item' = l,SPBmind (strengthen_mind env mp l mib) in - let rest' = strengthen_sig env msid rest mp in - item'::rest' - | (l,SPBmodule mb) :: rest -> - let mp' = MPdot (mp,l) in - let item' = l,SPBmodule (strengthen_mod env mp' mb) in - let env' = add_module - (MPdot (MPself msid,l)) - (module_body_of_spec mb) - env - in - let rest' = strengthen_sig env' msid rest mp in - item'::rest' - | (l,SPBmodtype mty as item) :: rest -> - let env' = add_modtype - (make_kn (MPself msid) empty_dirpath 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 + (subst_key (map_msid msid mp) mb.mod_alias) + (map_msid msid mp) + | _ -> true, mb.mod_alias diff --git a/checker/modops.mli b/checker/modops.mli index 10b231f44..17b063e2a 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -45,6 +45,8 @@ val check_modpath_equiv : env -> module_path -> module_path -> unit val strengthen : env -> struct_expr_body -> module_path -> struct_expr_body +val update_subst : env -> module_body -> module_path -> bool * substitution + val error_incompatible_modtypes : module_type_body -> module_type_body -> 'a |