summaryrefslogtreecommitdiff
path: root/checker/mod_checking.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /checker/mod_checking.ml
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'checker/mod_checking.ml')
-rw-r--r--checker/mod_checking.ml305
1 files changed, 143 insertions, 162 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 24000591..23ba4893 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -31,7 +31,7 @@ let check_constant_declaration env kn cb =
(match cb.const_type with
NonPolymorphicType ty ->
let ty, cu = refresh_arity ty in
- let envty = add_constraints cu env' in
+ let envty = add_constraints cu env' in
let _ = infer_type envty ty in
(match cb.const_body with
| Some bd ->
@@ -58,19 +58,15 @@ let rec list_split_assoc k rev_before = function
| (k',b)::after when k=k' -> rev_before,b,after
| h::tail -> list_split_assoc k (h::rev_before) tail
-let rec list_fold_map2 f e = function
+let rec list_fold_map2 f e = function
| [] -> (e,[],[])
- | h::t ->
+ | h::t ->
let e',h1',h2' = f e h in
let e'',t1',t2' = list_fold_map2 f e' t in
e'',h1'::t1',h2'::t2'
-
-let check_alias (s1:substitution) s2 =
- if s1 <> s2 then failwith "Incorrect alias"
-
let check_definition_sub env cb1 cb2 =
- let check_type env t1 t2 =
+ let check_type env t1 t2 =
(* If the type of a constant is generated, it may mention
non-variable algebraic universes that the general conversion
@@ -81,7 +77,7 @@ let check_definition_sub env cb1 cb2 =
Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
Hence they don't have to be checked again *)
- let t1,t2 =
+ let t1,t2 =
if isArity t2 then
let (ctx2,s2) = destArity t2 in
match s2 with
@@ -135,38 +131,38 @@ let lookup_modtype mp env =
with Not_found ->
failwith ("Unknown module type: "^string_of_mp mp)
-
-let rec check_with env mtb with_decl =
+let rec check_with env mtb with_decl mp=
match with_decl with
- | With_definition_body _ ->
- check_with_aux_def env mtb with_decl;
- empty_subst
- | With_module_body _ ->
- check_with_aux_mod env mtb with_decl
+ | With_definition_body _ ->
+ check_with_aux_def env mtb with_decl mp;
+ mtb
+ | With_module_body _ ->
+ check_with_aux_mod env mtb with_decl mp;
+ mtb
-and check_with_aux_def env mtb with_decl =
- let msid,sig_b = match (eval_struct env mtb) with
- | SEBstruct(msid,sig_b) ->
- msid,sig_b
+and check_with_aux_def env mtb with_decl mp =
+ let sig_b = match mtb with
+ | SEBstruct(sig_b) ->
+ sig_b
| _ -> error_signature_expected mtb
in
- let id,idl = match with_decl with
- | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) ->
+ 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
+ | 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 env' = Modops.add_signature (MPself msid) before env in
+ let env' = Modops.add_signature mp before empty_delta_resolver env in
match with_decl with
| With_definition_body ([],_) -> assert false
- | With_definition_body ([id],c) ->
+ | With_definition_body ([id],c) ->
let cb = match spec with
SFBconst cb -> cb
| _ -> error_not_a_constant l
- in
+ in
check_definition_sub env' c cb
| With_definition_body (_::_,_) ->
let old = match spec with
@@ -179,9 +175,9 @@ and check_with_aux_def env mtb with_decl =
let new_with_decl = match with_decl with
With_definition_body (_,c) ->
With_definition_body (idl,c)
- | With_module_body (_,c,t,cst) ->
- With_module_body (idl,c,t,cst) in
- check_with_aux_def env' (type_of_mb env old) new_with_decl
+ | With_module_body (_,c) ->
+ With_module_body (idl,c) in
+ check_with_aux_def env' old.mod_type new_with_decl (MPdot(mp,l))
| Some msb ->
error_a_generative_module_expected l
end
@@ -190,46 +186,35 @@ and check_with_aux_def env mtb with_decl =
Not_found -> error_no_such_label l
| Reduction.NotConvertible -> error_with_incorrect l
-and check_with_aux_mod env mtb with_decl =
- let initmsid,msid,sig_b =
- match eval_struct env mtb with
- | SEBstruct(msid,sig_b) ->
- let msid'=(refresh_msid msid) in
- msid,msid',(subst_signature_msid msid (MPself(msid')) sig_b)
+and check_with_aux_mod env mtb with_decl mp =
+ let sig_b =
+ match mtb with
+ | SEBstruct(sig_b) ->
+ sig_b
| _ -> error_signature_expected mtb in
- let id,idl = match with_decl with
- | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) ->
+ 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
+ | 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 initmsid
+ | [] -> mp
| i::r -> MPdot(mp_rec r,label_of_id i)
- in
- let env' = Modops.add_signature (MPself msid) before env in
+ in
+ let env' = Modops.add_signature mp before empty_delta_resolver env in
match with_decl with
- | With_module_body ([],_,_,_) -> assert false
- | With_module_body ([id], mp,_,_) ->
- let old,alias = match spec with
- SFBmodule msb -> Some msb,None
- | SFBalias (mp',_,_) -> None,Some mp'
+ | With_module_body ([],_) -> assert false
+ | With_module_body ([id], mp1) ->
+ let _ = match spec with
+ SFBmodule msb -> msb
| _ -> error_not_a_module l
in
- let mtb' = lookup_modtype mp env' in
- let _ =
- match old,alias with
- Some msb,None -> ()
- | None,Some mp' ->
- check_modpath_equiv env' mp mp'
- | _,_ ->
- anomaly "Mod_typing:no implementation and no alias"
- in
- join (map_mp (mp_rec [id]) mp) mtb'.typ_alias
- | With_module_body (_::_,mp,_,_) ->
+ let _ = (lookup_module mp1 env) in ()
+ | With_module_body (_::_,mp) ->
let old = match spec with
SFBmodule msb -> msb
| _ -> error_not_a_module l
@@ -238,14 +223,12 @@ and check_with_aux_mod env mtb with_decl =
match old.mod_expr with
None ->
let new_with_decl = match with_decl with
- With_definition_body (_,c) ->
+ With_definition_body (_,c) ->
With_definition_body (idl,c)
- | With_module_body (_,c,t,cst) ->
- With_module_body (idl,c,t,cst) in
- let sub =
- check_with_aux_mod env'
- (type_of_mb env old) new_with_decl in
- join (map_mp (mp_rec idl) mp) sub
+ | With_module_body (_,c) ->
+ With_module_body (idl,c) in
+ check_with_aux_mod env'
+ old.mod_type new_with_decl (MPdot(mp,l))
| Some msb ->
error_a_generative_module_expected l
end
@@ -255,113 +238,111 @@ and check_with_aux_mod env mtb with_decl =
| Reduction.NotConvertible -> error_with_incorrect l
and check_module_type env mty =
- if mty.typ_strength <> None then
- failwith "strengthening of module types not supported";
- let sub = check_modexpr env mty.typ_expr in
- check_alias mty.typ_alias sub
+ let _ = check_modtype env mty.typ_expr mty.typ_mp in ()
-and check_module env mb =
- let sub =
- match mb.mod_expr, mb.mod_type with
- | None, None ->
- anomaly "Mod_typing.translate_module: empty type and expr in module entry"
- | None, Some mtb -> check_modexpr env mtb
-
- | Some mexpr, _ ->
- let sub1 = check_modexpr env mexpr in
- (match mb.mod_type with
- | None -> sub1
- | Some mte ->
- let sub2 = check_modexpr env mte in
- check_subtypes env
- {typ_expr = mexpr;
- typ_strength = None;
- typ_alias = sub1;}
- {typ_expr = mte;
- typ_strength = None;
- typ_alias = sub2;};
- sub2) in
- check_alias mb.mod_alias sub
-
-and check_structure_field (s,env) mp lab = function
+
+and check_module env mp mb =
+ match mb.mod_expr, mb.mod_type with
+ | None,mtb ->
+ let _ = check_modtype env mtb mb.mod_mp in ()
+ | Some mexpr, mtb when mtb==mexpr ->
+ let _ = check_modtype env mtb mb.mod_mp in ()
+ | Some mexpr, _ ->
+ let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in
+ let _ = check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in
+ check_subtypes env
+ {typ_mp=mp;
+ typ_expr=sign;
+ typ_expr_alg=None;
+ typ_constraints=Univ.Constraint.empty;
+ typ_delta = mb.mod_delta;}
+ {typ_mp=mp;
+ typ_expr=mb.mod_type;
+ typ_expr_alg=None;
+ typ_constraints=Univ.Constraint.empty;
+ typ_delta = mb.mod_delta;};
+
+and check_structure_field env mp lab res = function
| SFBconst cb ->
let c = make_con mp empty_dirpath lab in
- (s,check_constant_declaration env c cb)
+ check_constant_declaration env c cb
| SFBmind mib ->
- let kn = make_kn mp empty_dirpath lab in
- (s,Indtypes.check_inductive env kn mib)
+ let kn = make_mind mp empty_dirpath lab in
+ let kn = mind_of_delta res kn in
+ Indtypes.check_inductive env kn mib
| SFBmodule msb ->
- check_module env msb;
- 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 env)
- | SFBalias(mp2,_,cst) ->
- (* cf Safe_typing.add_alias *)
- (try
- let mp' = MPdot(mp,lab) in
- let mp2' = scrape_alias mp2 env in
- let _,sub = Modops.update_subst env (lookup_module mp2' env) mp2' in
- let sub = update_subst sub (map_mp mp' mp2') in
- let sub = join_alias sub (map_mp mp' mp2') in
- let sub = add_mp mp' mp2' sub in
- (join s sub, register_alias mp' mp2 env)
- with Not_found -> failwith "unknown aliased module")
+ let _= check_module env (MPdot(mp,lab)) msb in
+ Modops.add_module msb env
| SFBmodtype mty ->
- let kn = MPdot(mp, lab) in
check_module_type env mty;
- (join s mty.typ_alias, add_modtype kn mty env)
-
-and check_modexpr env mse = match mse with
+ add_modtype (MPdot(mp,lab)) mty env
+
+and check_modexpr env mse mp_mse res = match mse with
+ | SEBident mp ->
+ let mb = lookup_module mp env in
+ (subst_and_strengthen mb mp_mse env).mod_type
+ | SEBfunctor (arg_id, mtb, body) ->
+ check_module_type env mtb ;
+ let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
+ let sign = check_modexpr env' body mp_mse res in
+ SEBfunctor (arg_id, mtb, sign)
+ | SEBapply (f,m,cst) ->
+ let sign = check_modexpr env f mp_mse res in
+ let farg_id, farg_b, fbody_b = destr_functor env sign in
+ let mp =
+ try (path_of_mexpr m)
+ with Not_path -> error_application_to_not_path m
+ (* place for nondep_supertype *) in
+ let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in
+ check_subtypes env mtb farg_b;
+ (subst_struct_expr (map_mbid farg_id mp) fbody_b)
+ | SEBwith(mte, with_decl) ->
+ let sign = check_modexpr env mte mp_mse res in
+ let sign = check_with env sign with_decl mp_mse in
+ sign
+ | SEBstruct(msb) ->
+ let _ = List.fold_left (fun env (lab,mb) ->
+ check_structure_field env mp_mse lab res mb) env msb in
+ SEBstruct(msb)
+
+and check_modtype env mse mp_mse res = match mse with
| SEBident mp ->
- let mp = scrape_alias mp env in
let mtb = lookup_modtype mp env in
- mtb.typ_alias
+ mtb.typ_expr
| SEBfunctor (arg_id, mtb, body) ->
check_module_type env mtb;
- let env' = add_module (MPbound arg_id) (module_body_of_type mtb) env in
- let sub = check_modexpr env' body in
- sub
+ let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
+ let body = check_modtype env' body mp_mse res in
+ SEBfunctor(arg_id,mtb,body)
| 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 sign = check_modtype env f mp_mse res in
+ let farg_id, farg_b, fbody_b = destr_functor env sign in
let mp =
- try scrape_alias (path_of_mexpr m) env
+ try (path_of_mexpr m)
with Not_path -> error_application_to_not_path m
- (* place for nondep_supertype *) in
- let mtb = lookup_modtype mp env in
- check_subtypes env mtb farg_b;
- 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
+ (* place for nondep_supertype *) in
+ let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in
+ check_subtypes env mtb farg_b;
+ subst_struct_expr (map_mbid farg_id mp) fbody_b
| SEBwith(mte, with_decl) ->
- let sub1 = check_modexpr env mte in
- let sub2 = check_with env mte with_decl in
- join sub1 sub2
- | SEBstruct(msid,msb) ->
- let mp = MPself msid in
- let (sub,_) =
- List.fold_left (fun env (lab,mb) ->
- check_structure_field env mp lab mb) (empty_subst,env) msb in
- sub
-
+ let sign = check_modtype env mte mp_mse res in
+ let sign = check_with env sign with_decl mp_mse in
+ sign
+ | SEBstruct(msb) ->
+ let _ = List.fold_left (fun env (lab,mb) ->
+ check_structure_field env mp_mse lab res mb) env msb in
+ SEBstruct(msb)
+
(*
-let rec add_struct_expr_constraints env = function
+ let rec add_struct_expr_constraints env = function
| SEBident _ -> env
-
- | SEBfunctor (_,mtb,meb) ->
- add_struct_expr_constraints
- (add_modtype_constraints env mtb) meb
+
+ | SEBfunctor (_,mtb,meb) ->
+ add_struct_expr_constraints
+ (add_modtype_constraints env mtb) meb
| SEBstruct (_,structure_body) ->
- List.fold_left
+ List.fold_left
(fun env (l,item) -> add_struct_elem_constraints env item)
env
structure_body
@@ -369,20 +350,20 @@ let rec add_struct_expr_constraints env = function
| SEBapply (meb1,meb2,cst) ->
(* let g = Univ.merge_constraints cst Univ.initial_universes in
msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++
- Univ.pr_universes g++str"============="++fnl());
+ Univ.pr_universes g++str"============="++fnl());
*)
- Environ.add_constraints cst
- (add_struct_expr_constraints
- (add_struct_expr_constraints env meb1)
+ Environ.add_constraints cst
+ (add_struct_expr_constraints
+ (add_struct_expr_constraints env meb1)
meb2)
| SEBwith(meb,With_definition_body(_,cb))->
Environ.add_constraints cb.const_constraints
(add_struct_expr_constraints env meb)
| SEBwith(meb,With_module_body(_,_,cst))->
Environ.add_constraints cst
- (add_struct_expr_constraints env meb)
-
-and add_struct_elem_constraints env = function
+ (add_struct_expr_constraints env meb)
+
+and add_struct_elem_constraints env = function
| SFBconst cb -> Environ.add_constraints cb.const_constraints env
| SFBmind mib -> Environ.add_constraints mib.mind_constraints env
| SFBmodule mb -> add_module_constraints env mb
@@ -390,18 +371,18 @@ and add_struct_elem_constraints env = function
| SFBalias (mp,None) -> env
| SFBmodtype mtb -> add_modtype_constraints env mtb
-and add_module_constraints env mb =
+and add_module_constraints env mb =
let env = match mb.mod_expr with
| None -> env
| Some meb -> add_struct_expr_constraints env meb
in
let env = match mb.mod_type with
| None -> env
- | Some mtb ->
+ | Some mtb ->
add_struct_expr_constraints env mtb
in
Environ.add_constraints mb.mod_constraints env
-and add_modtype_constraints env mtb =
+and add_modtype_constraints env mtb =
add_struct_expr_constraints env mtb.typ_expr
*)