diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check_stat.ml | 2 | ||||
| -rw-r--r-- | checker/closure.ml | 2 | ||||
| -rw-r--r-- | checker/declarations.ml | 715 | ||||
| -rw-r--r-- | checker/declarations.mli | 39 | ||||
| -rw-r--r-- | checker/environ.ml | 46 | ||||
| -rw-r--r-- | checker/environ.mli | 13 | ||||
| -rw-r--r-- | checker/indtypes.ml | 6 | ||||
| -rw-r--r-- | checker/inductive.ml | 2 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 254 | ||||
| -rw-r--r-- | checker/modops.ml | 412 | ||||
| -rw-r--r-- | checker/modops.mli | 24 | ||||
| -rw-r--r-- | checker/safe_typing.ml | 15 | ||||
| -rw-r--r-- | checker/subtyping.ml | 188 | ||||
| -rw-r--r-- | checker/term.ml | 2 | ||||
| -rw-r--r-- | checker/typeops.ml | 4 |
15 files changed, 873 insertions, 851 deletions
diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 290e6ff8e0..170ac6384e 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -33,7 +33,7 @@ let pr_engt = function str "Theory: Set is predicative" let cst_filter f csts = - Cmap.fold + Cmap_env.fold (fun c ce acc -> if f c ce then c::acc else acc) csts [] diff --git a/checker/closure.ml b/checker/closure.ml index b55c5848eb..c710df816e 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -378,7 +378,7 @@ let defined_rels flags env = (rel_context env) ~init:(0,[]) (* else (0,[])*) -let mind_equiv_infos info = mind_equiv info.i_env +let mind_equiv_infos info = eq_ind let create mk_cl flgs env = { i_flags = flgs; diff --git a/checker/declarations.ml b/checker/declarations.ml index 0066e78489..3211cc28f5 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -31,60 +31,241 @@ let val_cst_type = type substitution_domain = - MSI of mod_self_id | MBI of mod_bound_id | MPI of module_path let val_subst_dom = - val_sum "substitution_domain" 0 [|[|val_uid|];[|val_uid|];[|val_mp|]|] + val_sum "substitution_domain" 0 [|[|val_uid|];[|val_mp|]|] module Umap = Map.Make(struct type t = substitution_domain let compare = Pervasives.compare end) -type resolver -type substitution = (module_path * resolver option) Umap.t +type delta_hint = + Inline of constr option + | Equiv of kernel_name + | Prefix_equiv of module_path + +type delta_key = + KN of kernel_name + | MP of module_path + +module Deltamap = Map.Make(struct + type t = delta_key + let compare = Pervasives.compare + end) + +type delta_resolver = delta_hint Deltamap.t + +let empty_delta_resolver = Deltamap.empty + +type substitution = (module_path * delta_resolver) Umap.t type 'a subst_fun = substitution -> 'a -> 'a -let val_res = val_opt no_val +let val_res_dom = no_val + (*val_sum "resolver_domain" 0 [|[|val_kn|];[|val_mp|]|]*) + +let val_res = no_val + (* val_map ~name:"delta_resolver" + val_res_dom + (val_sum "resolver_codomain" 0 [|[|val_opt val_constr||];[|val_kn|];[|val_mp|]|])*) let val_subst = val_map ~name:"substitution" val_subst_dom (val_tuple "substition range" [|val_mp;val_res|]) -let fold_subst fs fb fp = +let fold_subst fb fp = Umap.fold (fun k (mp,_) acc -> match k with - MSI msid -> fs msid mp acc | MBI mbid -> fb mbid mp acc | MPI mp1 -> fp mp1 mp acc) let empty_subst = Umap.empty -let add_msid msid mp = - Umap.add (MSI msid) (mp,None) let add_mbid mbid mp = - Umap.add (MBI mbid) (mp,None) + Umap.add (MBI mbid) (mp,empty_delta_resolver) let add_mp mp1 mp2 = - Umap.add (MPI mp1) (mp2,None) + Umap.add (MPI mp1) (mp2,empty_delta_resolver) -let map_msid msid mp = add_msid msid mp empty_subst let map_mbid mbid mp = add_mbid mbid mp empty_subst let map_mp mp1 mp2 = add_mp mp1 mp2 empty_subst +let add_inline_delta_resolver con = + Deltamap.add (KN(user_con con)) (Inline None) + +let add_inline_constr_delta_resolver con cstr = + Deltamap.add (KN(user_con con)) (Inline (Some cstr)) + +let add_constant_delta_resolver con = + Deltamap.add (KN(user_con con)) (Equiv (canonical_con con)) + +let add_mind_delta_resolver mind = + Deltamap.add (KN(user_mind mind)) (Equiv (canonical_mind mind)) + +let add_mp_delta_resolver mp1 mp2 = + Deltamap.add (MP mp1) (Prefix_equiv mp2) + +let mp_in_delta mp = + Deltamap.mem (MP mp) + +let con_in_delta con resolver = +try + match Deltamap.find (KN(user_con con)) resolver with + | Inline _ | Prefix_equiv _ -> false + | Equiv _ -> true +with + Not_found -> false + +let mind_in_delta mind resolver = +try + match Deltamap.find (KN(user_mind mind)) resolver with + | Inline _ | Prefix_equiv _ -> false + | Equiv _ -> true +with + Not_found -> false + +let delta_of_mp resolve mp = + try + match Deltamap.find (MP mp) resolve with + | Prefix_equiv mp1 -> mp1 + | _ -> anomaly "mod_subst: bad association in delta_resolver" + with + Not_found -> mp + +let delta_of_kn resolve kn = + try + match Deltamap.find (KN kn) resolve with + | Equiv kn1 -> kn1 + | Inline _ -> kn + | _ -> anomaly + "mod_subst: bad association in delta_resolver" + with + Not_found -> kn + +let remove_mp_delta_resolver resolver mp = + Deltamap.remove (MP mp) resolver + +exception Inline_kn + +let rec find_prefix resolve mp = + let rec sub_mp = function + | MPdot(mp,l) as mp_sup -> + (try + match Deltamap.find (MP mp_sup) resolve with + | Prefix_equiv mp1 -> mp1 + | _ -> anomaly + "mod_subst: bad association in delta_resolver" + with + Not_found -> MPdot(sub_mp mp,l)) + | p -> + match Deltamap.find (MP p) resolve with + | Prefix_equiv mp1 -> mp1 + | _ -> anomaly + "mod_subst: bad association in delta_resolver" + in + try + sub_mp mp + with + Not_found -> mp + +let solve_delta_kn resolve kn = + try + match Deltamap.find (KN kn) resolve with + | Equiv kn1 -> kn1 + | Inline _ -> raise Inline_kn + | _ -> anomaly + "mod_subst: bad association in delta_resolver" + with + Not_found | Inline_kn -> + let mp,dir,l = repr_kn kn in + let new_mp = find_prefix resolve mp in + if mp == new_mp then + kn + else + make_kn new_mp dir l + + +let constant_of_delta resolve con = + let kn = user_con con in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + con + else + constant_of_kn_equiv kn new_kn + +let constant_of_delta2 resolve con = + let kn = canonical_con con in + let kn1 = user_con con in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + con + else + constant_of_kn_equiv kn1 new_kn + +let mind_of_delta resolve mind = + let kn = user_mind mind in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + mind + else + mind_of_kn_equiv kn new_kn + +let mind_of_delta2 resolve mind = + let kn = canonical_mind mind in + let kn1 = user_mind mind in + let new_kn = solve_delta_kn resolve kn in + if kn == new_kn then + mind + else + mind_of_kn_equiv kn1 new_kn + + + +let inline_of_delta resolver = + let extract key hint l = + match key,hint with + |KN kn, Inline _ -> kn::l + | _,_ -> l + in + Deltamap.fold extract resolver [] + +exception Not_inline + +let constant_of_delta_with_inline resolve con = + let kn1,kn2 = canonical_con con,user_con con in + try + match Deltamap.find (KN kn2) resolve with + | Inline None -> None + | Inline (Some const) -> Some const + | _ -> raise Not_inline + with + Not_found | Not_inline -> + try match Deltamap.find (KN kn1) resolve with + | Inline None -> None + | Inline (Some const) -> Some const + | _ -> raise Not_inline + with + Not_found | Not_inline -> None + let subst_mp0 sub mp = (* 's like subst *) let rec aux mp = match mp with - | MPself sid -> - let mp',resolve = Umap.find (MSI sid) sub in + | MPfile sid -> + let mp',resolve = Umap.find (MPI (MPfile sid)) sub in mp',resolve | MPbound bid -> - let mp',resolve = Umap.find (MBI bid) sub in - mp',resolve + begin + try + let mp',resolve = Umap.find (MBI bid) sub in + mp',resolve + with Not_found -> + let mp',resolve = Umap.find (MPI mp) sub in + mp',resolve + end | MPdot (mp1,l) as mp2 -> begin try @@ -94,59 +275,135 @@ let subst_mp0 sub mp = (* 's like subst *) let mp1',resolve = aux mp1 in MPdot (mp1',l),resolve end - | _ -> raise Not_found in try Some (aux mp) with Not_found -> None - - -let subst_mp0 sub mp = (* 's like subst *) - let rec aux mp = - match mp with - | MPself sid -> fst (Umap.find (MSI sid) sub) - | MPbound bid -> fst (Umap.find (MBI bid) sub) - | MPdot (mp1,l) as mp2 -> - begin - try fst (Umap.find (MPI mp2) sub) - with Not_found -> MPdot (aux mp1,l) - end - - | _ -> raise Not_found - in - try Some (aux mp) with Not_found -> None - let subst_mp sub mp = match subst_mp0 sub mp with None -> mp - | Some mp' -> mp' + | Some (mp',_) -> mp' -let subst_kn0 sub kn = +let subst_kn_delta sub kn = let mp,dir,l = repr_kn kn in match subst_mp0 sub mp with - Some mp' -> - Some (make_kn mp' dir l) - | None -> None + Some (mp',resolve) -> + solve_delta_kn resolve (make_kn mp' dir l) + | None -> kn let subst_kn sub kn = - match subst_kn0 sub kn with - None -> kn - | Some kn' -> kn' + let mp,dir,l = repr_kn kn in + match subst_mp0 sub mp with + Some (mp',_) -> + make_kn mp' dir l + | None -> kn + +exception No_subst + +type sideconstantsubst = + | User + | Canonical + +let subst_ind sub mind = + let kn1,kn2 = user_mind mind,canonical_mind mind in + let mp1,dir,l = repr_kn kn1 in + let mp2,_,_ = repr_kn kn2 in + try + let side,mind',resolve = + match subst_mp0 sub mp1,subst_mp0 sub mp2 with + None,None ->raise No_subst + | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve + | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve + | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, + (make_mind_equiv mp1' mp2' dir l), resolve2 + in + match side with + |User -> + let mind = mind_of_delta resolve mind' in + mind + |Canonical -> + let mind = mind_of_delta2 resolve mind' in + mind + with + No_subst -> mind + +let subst_mind0 sub mind = + let kn1,kn2 = user_mind mind,canonical_mind mind in + let mp1,dir,l = repr_kn kn1 in + let mp2,_,_ = repr_kn kn2 in + try + let side,mind',resolve = + match subst_mp0 sub mp1,subst_mp0 sub mp2 with + None,None ->raise No_subst + | Some (mp',resolve),None -> User,(make_mind_equiv mp' mp2 dir l), resolve + | None, Some(mp',resolve)-> Canonical,(make_mind_equiv mp1 mp' dir l), resolve + | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, + (make_mind_equiv mp1' mp2' dir l), resolve2 + in + match side with + |User -> + let mind = mind_of_delta resolve mind' in + Some mind + |Canonical -> + let mind = mind_of_delta2 resolve mind' in + Some mind + with + No_subst -> Some mind let subst_con sub con = - let mp,dir,l = repr_con con in - match subst_mp0 sub mp with - None -> con - | Some mp' -> make_con mp' dir l + let kn1,kn2 = user_con con,canonical_con con in + let mp1,dir,l = repr_kn kn1 in + let mp2,_,_ = repr_kn kn2 in + try + let side,con',resolve = + match subst_mp0 sub mp1,subst_mp0 sub mp2 with + None,None ->raise No_subst + | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve + | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve + | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, + (make_con_equiv mp1' mp2' dir l), resolve2 + in + match constant_of_delta_with_inline resolve con' with + None -> begin + match side with + |User -> + let con = constant_of_delta resolve con' in + con,Const con + |Canonical -> + let con = constant_of_delta2 resolve con' in + con,Const con + end + | Some t -> con',t + with No_subst -> con , Const con + let subst_con0 sub con = - let mp,dir,l = repr_con con in - match subst_mp0 sub mp with - None -> None - | Some mp' -> - let con' = make_con mp' dir l in - Some (Const con') + let kn1,kn2 = user_con con,canonical_con con in + let mp1,dir,l = repr_kn kn1 in + let mp2,_,_ = repr_kn kn2 in + try + let side,con',resolve = + match subst_mp0 sub mp1,subst_mp0 sub mp2 with + None,None ->raise No_subst + | Some (mp',resolve),None -> User,(make_con_equiv mp' mp2 dir l), resolve + | None, Some(mp',resolve)-> Canonical,(make_con_equiv mp1 mp' dir l), resolve + | Some(mp1',resolve1),Some(mp2',resolve2)->Canonical, + (make_con_equiv mp1' mp2' dir l), resolve2 + in + match constant_of_delta_with_inline resolve con' with + None ->begin + match side with + |User -> + let con = constant_of_delta resolve con' in + Some (Const con) + |Canonical -> + let con = constant_of_delta2 resolve con' in + Some (Const con) + end + | t -> t + with No_subst -> Some (Const con) + let rec map_kn f f' c = let func = map_kn f f' in @@ -220,22 +477,8 @@ let rec map_kn f f' c = | _ -> c let subst_mps sub = - map_kn (subst_kn0 sub) (subst_con0 sub) + map_kn (subst_mind0 sub) (subst_con0 sub) -let rec replace_mp_in_mp mpfrom mpto mp = - match mp with - | _ when mp = mpfrom -> mpto - | MPdot (mp1,l) -> - let mp1' = replace_mp_in_mp mpfrom mpto mp1 in - if mp1==mp1' then mp - else MPdot (mp1',l) - | _ -> mp - -let replace_mp_in_con mpfrom mpto kn = - let mp,dir,l = kn in - let mp'' = replace_mp_in_mp mpfrom mpto mp in - if mp==mp'' then kn - else (mp'', dir, l) type 'a lazy_subst = | LSval of 'a @@ -253,117 +496,115 @@ let force fsubst r = r := LSval a'; a' - - -let join (subst1 : substitution) (subst2 : substitution) = - let apply_subst (sub : substitution) key (mp,_) = - match subst_mp0 sub mp with - None -> mp,None - | Some mp' -> mp',None in - let subst = Umap.mapi (apply_subst subst2) subst1 in - (Umap.fold Umap.add subst2 subst) - -let subst_key subst1 subst2 = - let replace_in_key key mp sub= - let newkey = - match key with - | MPI mp1 -> - begin - match subst_mp0 subst1 mp1 with - | None -> None - | Some mp2 -> Some (MPI mp2) - end - | _ -> None - in - match newkey with - | None -> Umap.add key mp sub - | Some mpi -> Umap.add mpi mp sub +let mp_in_key mp key = + let rec mp_rec mp1 = + match mp1 with + | _ when mp1 = mp -> true + | MPdot (mp2,l) -> mp_rec mp2 + | _ -> false + in + match key with + | MP mp1 -> + mp_rec mp1 + | KN kn -> + let mp1,dir,l = repr_kn kn in + mp_rec mp1 + +let subset_prefixed_by mp resolver = + let prefixmp key hint resolv = + if mp_in_key mp key then + Deltamap.add key hint resolv + else + resolv in - Umap.fold replace_in_key subst2 empty_subst - -let update_subst_alias subst1 subst2 = - let subst_inv key (mp,_) sub = - let newmp = - match key with - | MBI msid -> Some (MPbound msid) - | MSI msid -> Some (MPself msid) - | _ -> None - in - match newmp with - | None -> sub - | Some mpi -> match mp with - | MPbound mbid -> Umap.add (MBI mbid) (mpi,None) sub - | MPself msid -> Umap.add (MSI msid) (mpi,None) sub - | _ -> Umap.add (MPI mp) (mpi,None) sub + Deltamap.fold prefixmp resolver empty_delta_resolver + +let subst_dom_delta_resolver subst resolver = + let apply_subst key hint resolver = + match key with + (MP mp) -> + Deltamap.add (MP (subst_mp subst mp)) hint resolver + | (KN kn) -> + Deltamap.add (KN (subst_kn subst kn)) hint resolver in - let subst_mbi = Umap.fold subst_inv subst2 empty_subst in - let alias_subst key (mp,_) sub= - let newkey = - match key with - | MPI mp1 -> - begin - match subst_mp0 subst_mbi mp1 with - | None -> None - | Some mp2 -> Some (MPI mp2) - end - | _ -> None - in - match newkey with - | None -> Umap.add key (mp,None) sub - | Some mpi -> Umap.add mpi (mp,None) sub - in - Umap.fold alias_subst subst1 empty_subst + Deltamap.fold apply_subst resolver empty_delta_resolver -let join_alias (subst1 : substitution) (subst2 : substitution) = - let apply_subst (sub : substitution) key (mp,_) = - match subst_mp0 sub mp with - None -> mp,None - | Some mp' -> mp',None in - 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 +let subst_mp_delta sub mp key= + match subst_mp0 sub mp with + None -> empty_delta_resolver,mp + | Some (mp',resolve) -> + let mp1 = find_prefix resolve mp' in + let resolve1 = subset_prefixed_by mp1 resolve in + match key with + MP mpk -> + (subst_dom_delta_resolver + (map_mp mp1 mpk) resolve1),mp1 + | _ -> anomaly "Mod_subst: Bad association in resolver" + +let subst_codom_delta_resolver subst resolver = + let apply_subst key hint resolver = + match hint with + Prefix_equiv mp -> + let derived_resolve,mpnew = subst_mp_delta subst mp key in + Deltamap.fold Deltamap.add derived_resolve + (Deltamap.add key (Prefix_equiv mpnew) resolver) + | (Equiv kn) -> + Deltamap.add key (Equiv (subst_kn_delta subst kn)) resolver + | Inline None -> + Deltamap.add key hint resolver + | Inline (Some t) -> + Deltamap.add key (Inline (Some (subst_mps subst t))) resolver 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 + Deltamap.fold apply_subst resolver empty_delta_resolver + +let subst_dom_codom_delta_resolver subst resolver = + subst_dom_delta_resolver subst + (subst_codom_delta_resolver subst resolver) + +let update_delta_resolver resolver1 resolver2 = + let apply_res key hint res = + try + match hint with + Prefix_equiv mp -> + let new_hint = + Prefix_equiv (find_prefix resolver2 mp) + in Deltamap.add key new_hint res + | Equiv kn -> + let new_hint = + Equiv (solve_delta_kn resolver2 kn) + in Deltamap.add key new_hint res + | _ -> Deltamap.add key hint res + with not_found -> + Deltamap.add key hint res 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 + Deltamap.fold apply_res resolver1 empty_delta_resolver + +let add_delta_resolver resolver1 resolver2 = + if resolver1 == resolver2 then + resolver2 + else + Deltamap.fold Deltamap.add (update_delta_resolver resolver1 resolver2) + resolver2 +let join (subst1 : substitution) (subst2 : substitution) = + let apply_subst (sub : substitution) key (mp,resolve) = + let mp',resolve' = + match subst_mp0 sub mp with + None -> mp, None + | Some (mp',resolve') -> mp' + ,Some resolve' in + let resolve'' : delta_resolver = + match resolve' with + Some res -> + add_delta_resolver + (subst_dom_codom_delta_resolver sub resolve) + res + | None -> + subst_codom_delta_resolver sub resolve + in + mp',resolve'' in + let subst = Umap.mapi (apply_subst subst2) subst1 in + (Umap.fold Umap.add subst2 subst) let subst_substituted s r = match !r with @@ -414,7 +655,7 @@ let val_recarg = val_sum "recarg" 1 (* Norec *) let subst_recarg sub r = match r with | Norec | Mrec _ -> r - | Imbr (kn,i) -> let kn' = subst_kn sub kn in + | Imbr (kn,i) -> let kn' = subst_ind sub kn in if kn==kn' then r else Imbr (kn',i) type wf_paths = recarg Rtree.t @@ -547,8 +788,6 @@ type mutual_inductive_body = { (* Universes constraints enforced by the inductive declaration *) mind_constraints : Univ.constraints; - (* Source of the inductive block when aliased in a module *) - mind_equiv : kernel_name option } let val_ind_pack = val_tuple "mutual_inductive_body" [|val_array val_one_ind;val_bool;val_bool;val_int;val_nctxt; @@ -605,8 +844,7 @@ let subst_mind sub mib = mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt; mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ; - mind_constraints = mib.mind_constraints ; - mind_equiv = Option.map (subst_kn sub) mib.mind_equiv } + mind_constraints = mib.mind_constraints } (* Modules *) @@ -616,7 +854,6 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * struct_expr_body option * Univ.constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list @@ -624,116 +861,120 @@ and structure_body = (label * structure_field_body) list and struct_expr_body = | SEBident of module_path | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body - | SEBstruct of mod_self_id * structure_body - | SEBapply of struct_expr_body * struct_expr_body - * Univ.constraints + | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints + | SEBstruct of structure_body | SEBwith of struct_expr_body * with_declaration_body and with_declaration_body = - With_module_body of identifier list * module_path * - struct_expr_body option * Univ.constraints + With_module_body of identifier list * module_path | With_definition_body of identifier list * constant_body and module_body = - { mod_expr : struct_expr_body option; - mod_type : struct_expr_body option; + { mod_mp : module_path; + mod_expr : struct_expr_body option; + mod_type : struct_expr_body; + mod_type_alg : struct_expr_body option; mod_constraints : Univ.constraints; - mod_alias : substitution; + mod_delta : delta_resolver; mod_retroknowledge : action list} and module_type_body = - { typ_expr : struct_expr_body; - typ_strength : module_path option; - typ_alias : substitution} + { typ_mp : module_path; + typ_expr : struct_expr_body; + typ_expr_alg : struct_expr_body option ; + typ_constraints : Univ.constraints; + typ_delta :delta_resolver} (* the validation functions: *) let rec val_sfb o = val_sum "struct_field_body" 0 [|[|val_cb|]; (* SFBconst *) [|val_ind_pack|]; (* SFBmind *) [|val_module|]; (* SFBmodule *) - [|val_mp;val_opt val_seb;val_opt val_cstrs|]; (* SFBalias *) [|val_modtype|] (* SFBmodtype *) |] o and val_sb o = val_list (val_tuple"label*sfb"[|val_id;val_sfb|]) o and val_seb o = val_sum "struct_expr_body" 0 [|[|val_mp|]; (* SEBident *) [|val_uid;val_modtype;val_seb|]; (* SEBfunctor *) - [|val_uid;val_sb|]; (* SEBstruct *) + [|val_sb|]; (* SEBstruct *) [|val_seb;val_seb;val_cstrs|]; (* SEBapply *) [|val_seb;val_with|] (* SEBwith *) |] o and val_with o = val_sum "with_declaration_body" 0 - [|[|val_list val_id;val_mp;val_cstrs|]; + [|[|val_list val_id;val_mp|]; [|val_list val_id;val_cb|]|] o and val_module o = val_tuple "module_body" - [|val_opt val_seb;val_opt val_seb;val_cstrs;val_subst;no_val|] o + [|val_mp;val_opt val_seb;val_opt val_seb; + val_seb;val_cstrs;val_res;no_val|] o and val_modtype o = val_tuple "module_type_body" - [|val_seb;val_opt val_mp;val_subst|] o + [|val_mp;val_seb;val_opt val_seb;val_cstrs;val_res|] o 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 (subst_struct_expr sub) typ_opt,cst) + | With_module_body(id,mp) -> + With_module_body(id,subst_mp sub mp) | With_definition_body(id,cb) -> With_definition_body( id,subst_const_body sub cb) -and subst_modtype sub mtb = +and subst_modtype sub mtb= let typ_expr' = subst_struct_expr sub mtb.typ_expr in - if typ_expr'==mtb.typ_expr then - mtb + let typ_alg' = + Option.smartmap + (subst_struct_expr sub) mtb.typ_expr_alg in + let mp = subst_mp sub mtb.typ_mp + in + if typ_expr'==mtb.typ_expr && + typ_alg'==mtb.typ_expr_alg && mp==mtb.typ_mp then + mtb else - { mtb with - typ_expr = typ_expr'} - -and subst_structure sub sign = - let subst_body = function - SFBconst cb -> + {mtb with + typ_mp = mp; + typ_expr = typ_expr'; + typ_expr_alg = typ_alg'} + +and subst_structure sub sign = + let subst_body = function + SFBconst cb -> SFBconst (subst_const_body sub cb) - | SFBmind mib -> + | SFBmind mib -> SFBmind (subst_mind sub mib) - | SFBmodule mb -> - SFBmodule (subst_module sub mb) - | SFBmodtype mtb -> + | SFBmodule mb -> + SFBmodule (subst_module sub mb) + | SFBmodtype mtb -> SFBmodtype (subst_modtype sub mtb) - | SFBalias (mp,typ_opt ,cst) -> - 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 -and subst_module sub mb = - let mtb' = Option.smartmap (subst_struct_expr sub) mb.mod_type in - (* This is similar to the previous case. In this case we have - a module M in a signature that is knows to be equivalent to a module M' - (because the signature is "K with Module M := M'") and we are substituting - M' with some M''. *) - let me' = Option.smartmap (subst_struct_expr sub) mb.mod_expr in - let mb_alias = join_alias mb.mod_alias sub in - if mtb'==mb.mod_type && mb.mod_expr == me' - && mb_alias == mb.mod_alias - then mb else - { mod_expr = me'; - mod_type=mtb'; - mod_constraints=mb.mod_constraints; - mod_alias = mb_alias; - mod_retroknowledge=mb.mod_retroknowledge} +and subst_module sub mb = + let mtb' = subst_struct_expr sub mb.mod_type in + let typ_alg' = Option.smartmap + (subst_struct_expr sub ) mb.mod_type_alg in + let me' = Option.smartmap + (subst_struct_expr sub) mb.mod_expr in + let mp = subst_mp sub mb.mod_mp in + if mtb'==mb.mod_type && mb.mod_expr == me' + && mp == mb.mod_mp + then mb else + { mb with + mod_mp = mp; + mod_expr = me'; + mod_type_alg = typ_alg'; + mod_type=mtb'} and subst_struct_expr sub = function - | SEBident mp -> SEBident (subst_mp sub mp) - | SEBfunctor (msid, mtb, meb') -> - SEBfunctor(msid,subst_modtype sub mtb,subst_struct_expr sub meb') - | SEBstruct (msid,str)-> - SEBstruct(msid, subst_structure sub str) + | SEBident mp -> SEBident (subst_mp sub mp) + | SEBfunctor (mbid, mtb, meb') -> + SEBfunctor(mbid,subst_modtype sub mtb + ,subst_struct_expr sub meb') + | SEBstruct (str)-> + SEBstruct( subst_structure sub str) | SEBapply (meb1,meb2,cst)-> 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 = - subst_structure (map_msid msid mp) diff --git a/checker/declarations.mli b/checker/declarations.mli index 3d061b4c2c..bae7da9084 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -141,19 +141,18 @@ type mutual_inductive_body = { (* Universes constraints enforced by the inductive declaration *) mind_constraints : Univ.constraints; - (* Source of the inductive block when aliased in a module *) - mind_equiv : kernel_name option } (* Modules *) type substitution +type delta_resolver +val empty_delta_resolver : delta_resolver type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * struct_expr_body option * Univ.constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list @@ -161,32 +160,33 @@ and structure_body = (label * structure_field_body) list and struct_expr_body = | SEBident of module_path | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body - | SEBstruct of mod_self_id * structure_body - | SEBapply of struct_expr_body * struct_expr_body - * Univ.constraints + | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints + | SEBstruct of structure_body | SEBwith of struct_expr_body * with_declaration_body and with_declaration_body = - With_module_body of identifier list * module_path * - struct_expr_body option * Univ.constraints + With_module_body of identifier list * module_path | With_definition_body of identifier list * constant_body and module_body = - { mod_expr : struct_expr_body option; - mod_type : struct_expr_body option; + { mod_mp : module_path; + mod_expr : struct_expr_body option; + mod_type : struct_expr_body; + mod_type_alg : struct_expr_body option; mod_constraints : Univ.constraints; - mod_alias : substitution; + mod_delta : delta_resolver; mod_retroknowledge : action list} and module_type_body = - { typ_expr : struct_expr_body; - typ_strength : module_path option; - typ_alias : substitution} + { typ_mp : module_path; + typ_expr : struct_expr_body; + typ_expr_alg : struct_expr_body option ; + typ_constraints : Univ.constraints; + typ_delta :delta_resolver} (* Substitutions *) val fold_subst : - (mod_self_id -> module_path -> 'a -> 'a) -> (mod_bound_id -> module_path -> 'a -> 'a) -> (module_path -> module_path -> 'a -> 'a) -> substitution -> 'a -> 'a @@ -194,10 +194,8 @@ val fold_subst : type 'a subst_fun = substitution -> 'a -> 'a val empty_subst : substitution -val add_msid : mod_self_id -> module_path -> substitution -> substitution val add_mbid : mod_bound_id -> module_path -> substitution -> substitution val add_mp : module_path -> module_path -> substitution -> substitution -val map_msid : mod_self_id -> module_path -> substitution val map_mbid : mod_bound_id -> module_path -> substitution val map_mp : module_path -> module_path -> substitution @@ -206,14 +204,9 @@ val subst_mind : mutual_inductive_body subst_fun val subst_modtype : substitution -> module_type_body -> module_type_body val subst_struct_expr : substitution -> struct_expr_body -> struct_expr_body val subst_structure : substitution -> structure_body -> structure_body -val subst_signature_msid : - mod_self_id -> module_path -> structure_body -> structure_body +val subst_module : substitution -> module_body -> module_body 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 (* Validation *) val val_eng : Obj.t -> unit diff --git a/checker/environ.ml b/checker/environ.ml index 2d5ff3e43f..3d14b995b2 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -5,11 +5,10 @@ open Term open Declarations type globals = { - env_constants : constant_body Cmap.t; - env_inductives : mutual_inductive_body KNmap.t; + env_constants : constant_body Cmap_env.t; + env_inductives : mutual_inductive_body Mindmap_env.t; env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t; - env_alias : module_path MPmap.t } + env_modtypes : module_type_body MPmap.t} type stratification = { env_universes : universes; @@ -25,11 +24,10 @@ type env = { let empty_env = { env_globals = - { env_constants = Cmap.empty; - env_inductives = KNmap.empty; + { env_constants = Cmap_env.empty; + env_inductives = Mindmap_env.empty; env_modules = MPmap.empty; - env_modtypes = MPmap.empty; - env_alias = MPmap.empty }; + env_modtypes = MPmap.empty}; env_named_context = []; env_rel_context = []; env_stratification = @@ -108,11 +106,11 @@ let add_constraints c env = (* Global constants *) let lookup_constant kn env = - Cmap.find kn env.env_globals.env_constants + Cmap_env.find kn env.env_globals.env_constants let add_constant kn cs env = let new_constants = - Cmap.add kn cs env.env_globals.env_constants in + Cmap_env.add kn cs env.env_globals.env_constants in let new_globals = { env.env_globals with env_constants = new_constants } in @@ -145,26 +143,15 @@ let evaluable_constant cst env = (* Mutual Inductives *) let lookup_mind kn env = - KNmap.find kn env.env_globals.env_inductives - -let rec scrape_mind env kn = - match (lookup_mind kn env).mind_equiv with - | None -> kn - | Some kn' -> scrape_mind env kn' + Mindmap_env.find kn env.env_globals.env_inductives let add_mind kn mib env = - let new_inds = KNmap.add kn mib env.env_globals.env_inductives in + let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in let new_globals = { env.env_globals with env_inductives = new_inds } in { env with env_globals = new_globals } -let rec mind_equiv env (kn1,i1) (kn2,i2) = - let rec equiv kn1 kn2 = - kn1 = kn2 || - scrape_mind env kn1 = scrape_mind env kn2 in - i1 = i2 && equiv kn1 kn2 - (* Modules *) @@ -182,19 +169,6 @@ let shallow_add_module mp mb env = env_modules = new_mods } in { env with env_globals = new_globals } -let register_alias mp1 mp2 env = - let new_alias = MPmap.add mp1 mp2 env.env_globals.env_alias in - let new_globals = - { env.env_globals with - env_alias = new_alias } in - { env with env_globals = new_globals } - -let rec scrape_alias mp env = - try - let mp1 = MPmap.find mp env.env_globals.env_alias in - scrape_alias mp1 env - with - Not_found -> mp let lookup_module mp env = MPmap.find mp env.env_globals.env_modules diff --git a/checker/environ.mli b/checker/environ.mli index 1541bf0d82..776698ed85 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -4,12 +4,10 @@ open Term (* Environments *) type globals = { - env_constants : Declarations.constant_body Cmap.t; - env_inductives : Declarations.mutual_inductive_body KNmap.t; + env_constants : Declarations.constant_body Cmap_env.t; + env_inductives : Declarations.mutual_inductive_body Mindmap_env.t; env_modules : Declarations.module_body MPmap.t; - env_modtypes : Declarations.module_type_body MPmap.t; - env_alias : module_path MPmap.t; -} + env_modtypes : Declarations.module_type_body MPmap.t} type stratification = { env_universes : Univ.universes; env_engagement : Declarations.engagement option; @@ -61,17 +59,14 @@ val evaluable_constant : constant -> env -> bool (* Inductives *) val lookup_mind : mutual_inductive -> env -> Declarations.mutual_inductive_body -val scrape_mind : env -> mutual_inductive -> mutual_inductive + val add_mind : mutual_inductive -> Declarations.mutual_inductive_body -> env -> env -val mind_equiv : env -> inductive -> inductive -> bool (* Modules *) val add_modtype : module_path -> Declarations.module_type_body -> env -> env val shallow_add_module : module_path -> Declarations.module_body -> env -> env -val register_alias : module_path -> module_path -> env -> env -val scrape_alias : module_path -> env -> module_path val lookup_module : module_path -> env -> Declarations.module_body val lookup_modtype : module_path -> env -> Declarations.module_type_body diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 3d4f6be79e..e0aa9e7c31 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -22,13 +22,11 @@ open Environ let rec debug_string_of_mp = function | MPfile sl -> string_of_dirpath sl | MPbound uid -> "bound("^string_of_mbid uid^")" - | MPself uid -> "self("^string_of_msid uid^")" | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l let rec string_of_mp = function | MPfile sl -> string_of_dirpath sl | MPbound uid -> string_of_mbid uid - | MPself uid -> string_of_msid uid | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l let string_of_mp mp = @@ -515,7 +513,7 @@ let check_positivity env_ar params nrecp inds = (************************************************************************) let check_inductive env kn mib = - Flags.if_verbose msgnl (str " checking ind: " ++ prkn kn); + Flags.if_verbose msgnl (str " checking ind: " ++ pr_mind kn); (* check mind_constraints: should be consistent with env *) let env = add_constraints mib.mind_constraints env in (* check mind_record : TODO ? check #constructor = 1 ? *) @@ -540,8 +538,6 @@ let check_inductive env kn mib = (* check mind_nparams_rec: positivity condition *) check_positivity env_ar params mib.mind_nparams_rec mib.mind_packets; (* check mind_equiv... *) - if mib.mind_equiv <> None then - msg_warning (str"TODO: mind_equiv not checked"); (* Now we can add the inductive *) add_mind kn mib env diff --git a/checker/inductive.ml b/checker/inductive.ml index e08efbe5b6..19c7a6cfe9 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -351,7 +351,7 @@ let type_case_branches env (ind,largs) (p,pj) c = let check_case_info env indsp ci = let (mib,mip) = lookup_mind_specif env indsp in if - not (mind_equiv env indsp ci.ci_ind) or + not (eq_ind indsp ci.ci_ind) or (mib.mind_nparams <> ci.ci_npar) or (mip.mind_consnrealdecls <> ci.ci_cstr_nargs) then raise (TypeError(env,WrongCaseInfo(indsp,ci))) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 99babe6322..e95109fc58 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -65,10 +65,6 @@ let rec list_fold_map2 f e = function 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 = @@ -135,31 +131,31 @@ 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 + check_with_aux_def env mtb with_decl mp; + mtb | With_module_body _ -> - check_with_aux_mod env mtb with_decl + 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,_,_,_) -> + | 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) -> @@ -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,_,_,_) -> + | 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 + 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 @@ -240,12 +225,10 @@ and check_with_aux_mod 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 - 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,110 +238,105 @@ 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 - -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 + let _ = check_modtype env mty.typ_expr mty.typ_mp in () + + +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, _ -> + let sign = check_modexpr env mexpr mb.mod_mp in + let _ = check_modtype env mb.mod_type mb.mod_mp in + check_subtypes env + {typ_mp=mp; + typ_expr=sign; + typ_expr_alg=None; + typ_constraints=Univ.Constraint.empty; + typ_delta = empty_delta_resolver;} + {typ_mp=mp; + typ_expr=mb.mod_type; + typ_expr_alg=None; + typ_constraints=Univ.Constraint.empty; + typ_delta = empty_delta_resolver;}; + +and check_structure_field env mp lab = 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 + 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 "unkown 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 = 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 in + SEBfunctor (arg_id, mtb, sign) + | SEBapply (f,m,cst) -> + let sign = check_modexpr env f mp_mse 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 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 mb) env msb in + SEBstruct(msb) + +and check_modtype env mse mp_mse= 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 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 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 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 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 + add_struct_expr_constraints + (add_modtype_constraints env mtb) meb | SEBstruct (_,structure_body) -> List.fold_left diff --git a/checker/modops.ml b/checker/modops.ml index a986e18981..3d07135d1d 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -32,11 +32,10 @@ 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 = user_err_loc (loc,"",str ("\""^string_of_label s^"\" is not a module")) @@ -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,157 @@ 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 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" +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 = []} -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_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) - -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 " - -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 " - -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 +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; + } + + +let rec strengthen_mod env mp_from mp_to mb = + assert(mp_from = mb.mod_mp); +(* if 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,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 strengthen env mtb mp = strengthen_mtb env mp mtb + | (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' + +let strengthen env mtb mp = +(* if mp_in_delta mtb.typ_mp mtb.typ_delta then + (* in this case mtb has already been strengthened*) + mtb + else*) + 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 " -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 subst_and_strengthen mb mp env = + strengthen_mod env mb.mod_mp mp + (subst_module (map_mp mb.mod_mp mp) mb) + + +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} diff --git a/checker/modops.mli b/checker/modops.mli index d5c9f4de6d..4476013c67 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -19,33 +19,25 @@ open Environ (* Various operations on modules and module types *) -(* make the environment entry out of type *) -val module_body_of_type : module_type_body -> module_body +(* make the envirconment entry out of type *) +val module_body_of_type : module_path -> module_type_body -> module_body -val module_type_of_module : module_path option -> module_body -> +val module_type_of_module : env -> module_path option -> module_body -> module_type_body val destr_functor : env -> struct_expr_body -> mod_bound_id * module_type_body * struct_expr_body -(* Evaluation functions *) -val eval_struct : env -> struct_expr_body -> struct_expr_body - -val type_of_mb : env -> module_body -> struct_expr_body - -(* [add_signature mp sign env] assumes that the substitution [msid] - $\mapsto$ [mp] has already been performed (or is not necessary, like - when [mp = MPself msid]) *) -val add_signature : module_path -> structure_body -> env -> env +val add_signature : module_path -> structure_body -> delta_resolver -> env -> env (* adds a module and its components, but not the constraints *) -val add_module : module_path -> module_body -> env -> env +val add_module : module_body -> env -> env val check_modpath_equiv : env -> module_path -> module_path -> unit -val strengthen : env -> struct_expr_body -> module_path -> struct_expr_body +val strengthen : env -> module_type_body -> module_path -> module_type_body -val update_subst : env -> module_body -> module_path -> bool * substitution +val subst_and_strengthen : module_body -> module_path -> env -> module_body val error_incompatible_modtypes : module_type_body -> module_type_body -> 'a @@ -57,7 +49,7 @@ val error_with_incorrect : label -> 'a val error_no_such_label : label -> 'a val error_no_such_label_sub : - label -> mod_self_id -> mod_self_id -> 'a + label -> module_path -> 'a val error_signature_expected : struct_expr_body -> 'a diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index b0d683ff3e..da0e63c237 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -30,9 +30,8 @@ let set_engagement c = (* full_add_module adds module with universes and constraints *) let full_add_module dp mb digest = let env = !genv in - let mp = MPfile dp in let env = add_constraints mb.mod_constraints env in - let env = Modops.add_module mp mb env in + let env = Modops.add_module mb env in genv := add_digest env dp digest (* Check that the engagement expected by a library matches the initial one *) @@ -66,16 +65,16 @@ let check_imports f caller env needed = (* Remove the body of opaque constants in modules *) -(* also remove mod_expr ? *) +(* also remove mod_expr ? Good idea!*) let rec lighten_module mb = { mb with mod_expr = Option.map lighten_modexpr mb.mod_expr; - mod_type = Option.map lighten_modexpr mb.mod_type } + mod_type = lighten_modexpr mb.mod_type } and lighten_struct struc = let lighten_body (l,body) = (l,match body with | SFBconst ({const_opaque=true} as x) -> SFBconst {x with const_body=None} - | (SFBconst _ | SFBmind _ | SFBalias _) as x -> x + | (SFBconst _ | SFBmind _ ) as x -> x | SFBmodule m -> SFBmodule (lighten_module m) | SFBmodtype m -> SFBmodtype ({m with @@ -90,8 +89,8 @@ and lighten_modexpr = function typ_expr = lighten_modexpr mty.typ_expr}), lighten_modexpr mexpr) | SEBident mp as x -> x - | SEBstruct (msid, struc) -> - SEBstruct (msid, lighten_struct struc) + | SEBstruct ( struc) -> + SEBstruct ( lighten_struct struc) | SEBapply (mexpr,marg,u) -> SEBapply (lighten_modexpr mexpr,lighten_modexpr marg,u) | SEBwith (seb,wdcl) -> @@ -125,7 +124,7 @@ let import file (dp,mb,depends,engmt as vo) digest = let env = !genv in check_imports msg_warning dp env depends; check_engagement env engmt; - check_module (add_constraints mb.mod_constraints env) mb; + check_module (add_constraints mb.mod_constraints env) mb.mod_mp mb; stamp_library file digest; (* We drop proofs once checked *) (* let mb = lighten_module mb in*) diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 88989b32eb..ec1c908a60 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -32,7 +32,6 @@ type namedobject = | IndConstr of constructor * mutual_inductive_body | Module of module_body | Modtype of module_type_body - | Alias of module_path * struct_expr_body option (* adds above information about one mutual inductive: all types and constructors *) @@ -60,13 +59,13 @@ let make_label_map mp list = match e with | SFBconst cb -> add_map (Constant cb) | SFBmind mib -> - add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map + add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map | SFBmodule mb -> add_map (Module mb) | SFBmodtype mtb -> add_map (Modtype mtb) - | SFBalias (mp,typ_opt,cst) -> add_map (Alias (mp,typ_opt)) in List.fold_right add_one list Labmap.empty + let check_conv_error error f env a1 a2 = try f env a1 a2 @@ -74,8 +73,8 @@ let check_conv_error error f env a1 a2 = NotConvertible -> error () (* for now we do not allow reorderings *) -let check_inductive env msid1 l info1 mib2 spec2 = - let kn = make_kn (MPself msid1) empty_dirpath l in +let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= + let kn = make_mind mp1 empty_dirpath l in let error () = error_not_match l spec2 in let check_conv f = check_conv_error error f in let mib1 = @@ -83,6 +82,7 @@ let check_inductive env msid1 l info1 mib2 spec2 = | IndType ((_,0), mib) -> mib | _ -> error () in + let mib2 = subst_mind subst2 mib2 in let check_inductive_type env t1 t2 = (* Due to sort-polymorphism in inductive types, the conclusions of @@ -155,7 +155,7 @@ let check_inductive env msid1 l info1 mib2 spec2 = (* the inductive types and constructors types have to be convertible *) check (fun mib -> mib.mind_nparams); - begin + (*begin match mib2.mind_equiv with | None -> () | Some kn2' -> @@ -165,7 +165,7 @@ let check_inductive env msid1 l info1 mib2 spec2 = | Some kn1' -> scrape_mind env kn1' in if kn1 <> kn2 then error () - end; + end;*) (* we check that records and their field names are preserved. *) check (fun mib -> mib.mind_record); if mib1.mind_record then begin @@ -187,7 +187,7 @@ let check_inductive env msid1 l info1 mib2 spec2 = let _ = array_map2_i check_cons_types mib1.mind_packets mib2.mind_packets in () -let check_constant env msid1 l info1 cb2 spec2 = +let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let error () = error_not_match l spec2 in let check_conv f = check_conv_error error f in let check_type env t1 t2 = @@ -236,30 +236,31 @@ let check_constant env msid1 l info1 cb2 spec2 = (t1,t2) in check_conv conv_leq env t1 t2 in - - match info1 with - | Constant cb1 -> - assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; - (*Start by checking types*) - let typ1 = Typeops.type_of_constant_type env cb1.const_type in - let typ2 = Typeops.type_of_constant_type env cb2.const_type in - check_type env typ1 typ2; - let con = make_con (MPself msid1) empty_dirpath l in - (match cb2 with - | {const_body=Some lc2;const_opaque=false} -> - let c2 = force_constr lc2 in - let c1 = match cb1.const_body with - | Some lc1 -> force_constr lc1 - | None -> Const con - in - check_conv conv env c1 c2 - | _ -> ()) - | IndType ((kn,i),mind1) -> - ignore (Util.error ( - "The kernel does not recognize yet that a parameter can be " ^ - "instantiated by an inductive type. Hint: you can rename the " ^ - "inductive type and give a definition to map the old name to the new " ^ - "name.")); + match info1 with + | Constant cb1 -> + assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; + (*Start by checking types*) + let cb1 = subst_const_body subst1 cb1 in + let cb2 = subst_const_body subst2 cb2 in + let typ1 = Typeops.type_of_constant_type env cb1.const_type in + let typ2 = Typeops.type_of_constant_type env cb2.const_type in + check_type env typ1 typ2; + let con = make_con mp1 empty_dirpath l in + (match cb2 with + | {const_body=Some lc2;const_opaque=false} -> + let c2 = force_constr lc2 in + let c1 = match cb1.const_body with + | Some lc1 -> force_constr lc1 + | None -> Const con + in + check_conv conv env c1 c2 + | _ -> ()) + | IndType ((kn,i),mind1) -> + ignore (Util.error ( + "The kernel does not recognize yet that a parameter can be " ^ + "instantiated by an inductive type. Hint: you can rename the " ^ + "inductive type and give a definition to map the old name to the new " ^ + "name.")); assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; if cb2.const_body <> None then error () ; let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in @@ -278,57 +279,31 @@ let check_constant env msid1 l info1 cb2 spec2 = check_conv conv env ty1 ty2 | _ -> error () -let rec check_modules env msid1 l msb1 msb2 = - let mp = (MPdot(MPself msid1,l)) in - let mty1 = module_type_of_module (Some mp) msb1 in - let mty2 = module_type_of_module None msb2 in - check_modtypes env mty1 mty2 false +let rec check_modules env msb1 msb2 subst1 subst2 = + let mty1 = module_type_of_module env None msb1 in + let mty2 = module_type_of_module env None msb2 in + check_modtypes env mty1 mty2 subst1 subst2 false; + - -and check_signatures env (msid1,sig1) alias (msid2,sig2') = - let mp1 = MPself msid1 in - let env = add_signature mp1 sig1 env in - let alias = update_subst_alias alias (map_msid msid2 mp1) in - let sig2 = subst_structure alias sig2' in - let sig2 = subst_signature_msid msid2 mp1 sig2 in +and check_signatures env mp1 sig1 sig2 subst1 subst2 = let map1 = make_label_map mp1 sig1 in - let check_one_body (l,spec2) = + let check_one_body (l,spec2) = let info1 = try Labmap.find l map1 with - Not_found -> error_no_such_label_sub l msid1 msid2 + Not_found -> error_no_such_label_sub l mp1 in match spec2 with | SFBconst cb2 -> - check_constant env msid1 l info1 cb2 spec2 + check_constant env mp1 l info1 cb2 spec2 subst1 subst2 | SFBmind mib2 -> - check_inductive env msid1 l info1 mib2 spec2 + check_inductive env mp1 l info1 mib2 spec2 subst1 subst2 | SFBmodule msb2 -> begin match info1 with - | Module msb -> check_modules env msid1 l msb msb2 - | Alias (mp,typ_opt) ->let msb = - {mod_expr = Some (SEBident mp); - mod_type = typ_opt; - mod_constraints = Constraint.empty; - mod_alias = (lookup_modtype mp env).typ_alias; - mod_retroknowledge = []} in - check_modules env msid1 l msb msb2 - | _ -> error_not_match l spec2 - end - | SFBalias (mp,typ_opt,_) -> - begin - match info1 with - | Alias (mp1,_) -> check_modpath_equiv env mp mp1 - | Module msb -> - let msb1 = - {mod_expr = Some (SEBident mp); - mod_type = typ_opt; - mod_constraints = Constraint.empty; - mod_alias = (lookup_modtype mp env).typ_alias; - mod_retroknowledge = []} in - check_modules env msid1 l msb msb1 + | Module msb -> check_modules env msb msb2 + subst1 subst2 | _ -> error_not_match l spec2 end | SFBmodtype mtb2 -> @@ -337,52 +312,61 @@ and check_signatures env (msid1,sig1) alias (msid2,sig2') = | Modtype mtb -> mtb | _ -> error_not_match l spec2 in - check_modtypes env mtb1 mtb2 true + let env = add_module (module_body_of_type mtb2.typ_mp mtb2) + (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in + check_modtypes env mtb1 mtb2 subst1 subst2 true in List.iter check_one_body sig2 -and check_modtypes env mtb1 mtb2 equiv = - if mtb1==mtb2 then () else (* just in case :) *) - let mtb1',mtb2'= - (match mtb1.typ_strength with - None -> eval_struct env mtb1.typ_expr, - eval_struct env mtb2.typ_expr - | Some mp -> strengthen env mtb1.typ_expr mp, - eval_struct env mtb2.typ_expr) in - let rec check_structure env str1 str2 equiv = - match str1, str2 with - | SEBstruct (msid1,list1), - SEBstruct (msid2,list2) -> - check_signatures env - (msid1,list1) mtb1.typ_alias (msid2,list2); - if equiv then - check_signatures env - (msid2,list2) mtb2.typ_alias (msid1,list1) +and check_modtypes env mtb1 mtb2 subst1 subst2 equiv = + if mtb1==mtb2 then () else + let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in + let rec check_structure env str1 str2 equiv subst1 subst2 = + match str1,str2 with + | SEBstruct (list1), + SEBstruct (list2) -> + check_signatures env + mtb1.typ_mp list1 list2 subst1 subst2; + if equiv then + check_signatures env + mtb2.typ_mp list2 list1 subst1 subst2 + else + () | SEBfunctor (arg_id1,arg_t1,body_t1), SEBfunctor (arg_id2,arg_t2,body_t2) -> - check_modtypes env arg_t2 arg_t1 equiv; + check_modtypes env + arg_t2 arg_t1 + (map_mp arg_t1.typ_mp arg_t2.typ_mp) subst2 + equiv ; (* contravariant *) - let env = - add_module (MPbound arg_id2) (module_body_of_type arg_t2) env + let env = add_module + (module_body_of_type (MPbound arg_id2) arg_t2) env in - let body_t1' = - (* since we are just checking well-typedness we do not need - to expand any constant. Hence the identity resolver. *) - subst_struct_expr - (map_mbid arg_id1 (MPbound arg_id2)) - body_t1 + let env = match body_t1 with + SEBstruct str -> + add_module {mod_mp = mtb1.typ_mp; + mod_expr = None; + mod_type = body_t1; + mod_type_alg= None; + mod_constraints=mtb1.typ_constraints; + mod_retroknowledge = []; + mod_delta = mtb1.typ_delta} env + | _ -> env in - check_structure env (eval_struct env body_t1') - (eval_struct env body_t2) equiv + check_structure env body_t1 body_t2 equiv + (join (map_mbid arg_id1 (MPbound arg_id2)) subst1) + subst2 | _ , _ -> error_incompatible_modtypes mtb1 mtb2 in if mtb1'== mtb2' then () - else check_structure env mtb1' mtb2' equiv + else check_structure env mtb1' mtb2' equiv subst1 subst2 let check_subtypes env sup super = (*if sup<>super then*) - check_modtypes env sup super false + check_modtypes env (strengthen env sup sup.typ_mp) super empty_subst + (map_mp super.typ_mp sup.typ_mp) false let check_equal env sup super = (*if sup<>super then*) - check_modtypes env sup super true + check_modtypes env sup super empty_subst + (map_mp super.typ_mp sup.typ_mp) true diff --git a/checker/term.ml b/checker/term.ml index 92d898b318..658eac4f00 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -489,7 +489,7 @@ let compare_constr f t1 t2 = f h1 h2 & List.for_all2 f l1 l2 else false | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2 - | Const c1, Const c2 -> c1 = c2 + | Const c1, Const c2 -> eq_constant c1 c2 | Ind c1, Ind c2 -> c1 = c2 | Construct c1, Construct c2 -> c1 = c2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> diff --git a/checker/typeops.ml b/checker/typeops.ml index 3a4f2f825d..e5cf6a6d6d 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -228,7 +228,7 @@ let judge_of_inductive_knowing_parameters env ind (paramstyp:constr array) = let (mib,mip) = try lookup_mind_specif env ind with Not_found -> - failwith ("Cannot find inductive: "^string_of_kn (fst ind)) in + failwith ("Cannot find inductive: "^string_of_mind (fst ind)) in check_args env c mib.mind_hyps; type_of_inductive_knowing_parameters env mip paramstyp @@ -244,7 +244,7 @@ let judge_of_constructor env c = let mib = try lookup_mind kn env with Not_found -> - failwith ("Cannot find inductive: "^string_of_kn (fst (fst c))) in + failwith ("Cannot find inductive: "^string_of_mind (fst (fst c))) in check_args env constr mib.mind_hyps in let specif = lookup_mind_specif env (inductive_of_constructor c) in type_of_constructor c specif |