aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-05-07 16:13:37 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-05-07 16:13:37 +0000
commitfa5fbb3625452dd560ffb5bfe5493d26b730b402 (patch)
tree357d6fe295e25a2c8b27d2d6911506ba3a6d590c /checker
parent335c779987e4b845e6700d5df81fe248e6e940f7 (diff)
fixed bug with aliases
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10896 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker')
-rw-r--r--checker/.depend166
-rw-r--r--checker/Makefile26
-rw-r--r--checker/check.ml10
-rw-r--r--checker/checker.ml9
-rw-r--r--checker/declarations.ml42
-rw-r--r--checker/declarations.mli1
-rw-r--r--checker/mod_checking.ml41
-rw-r--r--checker/modops.ml172
-rw-r--r--checker/modops.mli2
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