summaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/declarations.ml8
-rw-r--r--kernel/declarations.mli8
-rw-r--r--kernel/indtypes.ml5
-rw-r--r--kernel/indtypes.mli3
-rw-r--r--kernel/inductive.ml5
-rw-r--r--kernel/mod_typing.ml115
-rw-r--r--kernel/modops.ml115
-rw-r--r--kernel/names.ml14
-rw-r--r--kernel/names.mli5
-rw-r--r--kernel/safe_typing.ml15
-rw-r--r--kernel/subtyping.ml16
-rw-r--r--kernel/univ.ml23
12 files changed, 214 insertions, 118 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 6e99bf79..f4827029 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declarations.ml 10664 2008-03-14 11:27:37Z soubiran $ i*)
+(*i $Id: declarations.ml 11417 2008-09-17 15:06:57Z soubiran $ i*)
(*i*)
open Util
@@ -251,7 +251,8 @@ type structure_field_body =
| SFBconst of constant_body
| SFBmind of mutual_inductive_body
| SFBmodule of module_body
- | SFBalias of module_path * constraints option
+ | SFBalias of module_path * struct_expr_body option
+ * constraints option
| SFBmodtype of module_type_body
and structure_body = (label * structure_field_body) list
@@ -265,7 +266,8 @@ and struct_expr_body =
| SEBwith of struct_expr_body * with_declaration_body
and with_declaration_body =
- With_module_body of identifier list * module_path * constraints
+ With_module_body of identifier list * module_path
+ * struct_expr_body option * constraints
| With_definition_body of identifier list * constant_body
and module_body =
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index fa03a338..b4f5f1f7 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: declarations.mli 10664 2008-03-14 11:27:37Z soubiran $ i*)
+(*i $Id: declarations.mli 11417 2008-09-17 15:06:57Z soubiran $ i*)
(*i*)
open Names
@@ -181,7 +181,8 @@ type structure_field_body =
| SFBconst of constant_body
| SFBmind of mutual_inductive_body
| SFBmodule of module_body
- | SFBalias of module_path * constraints option
+ | SFBalias of module_path * struct_expr_body option
+ *constraints option
| SFBmodtype of module_type_body
and structure_body = (label * structure_field_body) list
@@ -195,7 +196,8 @@ and struct_expr_body =
| SEBwith of struct_expr_body * with_declaration_body
and with_declaration_body =
- With_module_body of identifier list * module_path * constraints
+ With_module_body of identifier list * module_path
+ * struct_expr_body option * constraints
| With_definition_body of identifier list * constant_body
and module_body =
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 01b8aca1..06764834 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: indtypes.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: indtypes.ml 11784 2009-01-14 11:36:32Z herbelin $ *)
open Util
open Names
@@ -46,6 +46,7 @@ type inductive_error =
| SameNamesOverlap of identifier list
| NotAnArity of identifier
| BadEntry
+ | LargeNonPropInductiveNotInType
exception InductiveError of inductive_error
@@ -266,7 +267,7 @@ let typecheck_inductive env mie =
| Prop Pos when engagement env <> Some ImpredicativeSet ->
(* Predicative set: check that the content is indeed predicative *)
if not (is_type0m_univ lev) & not (is_type0_univ lev) then
- error "Large non-propositional inductive types must be in Type.";
+ raise (InductiveError LargeNonPropInductiveNotInType);
Inl (info,full_arity,s), cst
| Prop _ ->
Inl (info,full_arity,s), cst in
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 0477df82..90ae70c3 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: indtypes.mli 10425 2008-01-05 17:04:16Z herbelin $ i*)
+(*i $Id: indtypes.mli 11784 2009-01-14 11:36:32Z herbelin $ i*)
(*i*)
open Names
@@ -33,6 +33,7 @@ type inductive_error =
| SameNamesOverlap of identifier list
| NotAnArity of identifier
| BadEntry
+ | LargeNonPropInductiveNotInType
exception InductiveError of inductive_error
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 4bb8e9d6..99ec1650 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: inductive.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: inductive.ml 11647 2008-12-02 10:40:11Z barras $ *)
open Util
open Names
@@ -683,7 +683,8 @@ let check_one_fix renv recpos def =
List.iter (check_rec_call renv) l
| Some c ->
try List.iter (check_rec_call renv) l
- with FixGuardError _ -> check_rec_call renv (applist(c,l))
+ with FixGuardError _ ->
+ check_rec_call renv (applist(lift p c,l))
end
| Case (ci,p,c_0,lrest) ->
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 6840febd..4a9fb606 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: mod_typing.ml 11170 2008-06-25 08:31:04Z soubiran $ i*)
+(*i $Id: mod_typing.ml 11514 2008-10-28 13:39:02Z soubiran $ i*)
open Util
open Names
@@ -37,14 +37,46 @@ 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 rec rebuild_mp mp l =
+ match l with
+ []-> mp
+ | i::r -> rebuild_mp (MPdot(mp,i)) r
+
+let type_of_struct env b meb =
+ let rec aux env = function
+ | SEBfunctor (mp,mtb,body) ->
+ let env = add_module (MPbound mp) (module_body_of_type mtb) env in
+ SEBfunctor(mp,mtb, aux env body)
+ | SEBident mp ->
+ strengthen env (lookup_modtype mp env).typ_expr mp
+ | SEBapply _ as mtb -> eval_struct env mtb
+ | str -> str
+ in
+ if b then
+ Some (aux env meb)
+ else
+ None
+
+let rec bounded_str_expr = function
+ | SEBfunctor (mp,mtb,body) -> bounded_str_expr body
+ | SEBident mp -> (check_bound_mp mp)
+ | SEBapply (f,a,_)->(bounded_str_expr f)
+ | _ -> false
+
+let return_opt_type mp env mtb =
+ if (check_bound_mp mp) then
+ Some (strengthen env mtb.typ_expr mp)
+ else
+ None
+
let rec check_with env mtb with_decl =
match with_decl with
| With_Definition (id,_) ->
let cb = check_with_aux_def env mtb with_decl in
SEBwith(mtb,With_definition_body(id,cb)),empty_subst
| With_Module (id,mp) ->
- let cst,sub = check_with_aux_mod env mtb with_decl true in
- SEBwith(mtb,With_module_body(id,mp,cst)),sub
+ let cst,sub,typ_opt = check_with_aux_mod env mtb with_decl true in
+ SEBwith(mtb,With_module_body(id,mp,typ_opt,cst)),sub
and check_with_aux_def env mtb with_decl =
let msid,sig_b = match (eval_struct env mtb) with
@@ -140,7 +172,7 @@ and check_with_aux_mod env mtb with_decl now =
| With_Module ([id], mp) ->
let old,alias = match spec with
SFBmodule msb -> Some msb,None
- | SFBalias (mp',cst) -> None,Some (mp',cst)
+ | SFBalias (mp',_,cst) -> None,Some (mp',cst)
| _ -> error_not_a_module (string_of_label l)
in
let mtb' = lookup_modtype mp env' in
@@ -164,35 +196,48 @@ and check_with_aux_mod env mtb with_decl now =
in
if now then
let mp' = scrape_alias mp env' in
- let up_subst = update_subst mtb'.typ_alias (map_mp (mp_rec [id]) mp') in
- cst, (join (map_mp (mp_rec [id]) mp') up_subst)
+ let _,sub = Modops.update_subst env' (module_body_of_type mtb') mp' in
+ let up_subst = update_subst sub (map_mp (mp_rec [id]) mp') in
+ cst, (join (map_mp (mp_rec [id]) mp') up_subst),(return_opt_type mp env' mtb')
else
- cst,empty_subst
+ cst,empty_subst,(return_opt_type mp env' mtb')
| With_Module (_::_,mp) ->
- let old = match spec with
- SFBmodule msb -> msb
+ let old,alias = match spec with
+ SFBmodule msb -> Some msb, None
+ | SFBalias (mpold,typ_opt,cst)->None, Some mpold
| _ -> error_not_a_module (string_of_label l)
in
begin
- match old.mod_expr with
- None ->
- let new_with_decl = match with_decl with
- With_Definition (_,c) ->
- With_Definition (idl,c)
- | With_Module (_,c) -> With_Module (idl,c) in
- let cst,_ =
- check_with_aux_mod env'
- (type_of_mb env old) new_with_decl false in
- if now then
- let mtb' = lookup_modtype mp env' in
- let mp' = scrape_alias mp env' in
- let up_subst = update_subst
- mtb'.typ_alias (map_mp (mp_rec (List.rev (id::idl))) mp') in
- cst, (join (map_mp (mp_rec (List.rev (id::idl))) mp') up_subst)
+ if alias = None then
+ let old = Option.get old in
+ match old.mod_expr with
+ None ->
+ let new_with_decl = match with_decl with
+ With_Definition (_,c) ->
+ With_Definition (idl,c)
+ | With_Module (_,c) -> With_Module (idl,c) in
+ let cst,_,typ_opt =
+ check_with_aux_mod env'
+ (type_of_mb env' old) new_with_decl false in
+ if now then
+ let mtb' = lookup_modtype mp env' in
+ let mp' = scrape_alias mp env' in
+ let _,sub = Modops.update_subst env' (module_body_of_type mtb') mp' in
+ let up_subst = update_subst
+ sub (map_mp (mp_rec (List.rev (id::idl))) mp') in
+ cst,
+ (join (map_mp (mp_rec (List.rev (id::idl))) mp') up_subst),
+ typ_opt
+ else
+ cst,empty_subst,typ_opt
+ | Some msb ->
+ error_a_generative_module_expected l
else
- cst,empty_subst
- | Some msb ->
- error_a_generative_module_expected l
+ let mpold = Option.get alias in
+ let mpnew = rebuild_mp mpold (List.map label_of_id idl) in
+ check_modpath_equiv env' mpnew mp;
+ let mtb' = lookup_modtype mp env' in
+ Constraint.empty,empty_subst,(return_opt_type mp env' mtb')
end
| _ -> anomaly "Modtyping:incorrect use of with"
with
@@ -214,7 +259,9 @@ and translate_module env me =
let meb,sub1 = translate_struct_entry env mexpr in
let mod_typ,sub,cst =
match me.mod_entry_type with
- | None -> None,sub1,Constraint.empty
+ | None ->
+ (type_of_struct env (bounded_str_expr meb) meb)
+ ,sub1,Constraint.empty
| Some mte ->
let mtb2,sub2 = translate_struct_entry env mte in
let cst = check_subtypes env
@@ -304,7 +351,7 @@ let rec add_struct_expr_constraints env = function
| SEBwith(meb,With_definition_body(_,cb))->
Environ.add_constraints cb.const_constraints
(add_struct_expr_constraints env meb)
- | SEBwith(meb,With_module_body(_,_,cst))->
+ | SEBwith(meb,With_module_body(_,_,_,cst))->
Environ.add_constraints cst
(add_struct_expr_constraints env meb)
@@ -312,8 +359,8 @@ 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
- | SFBalias (mp,Some cst) -> Environ.add_constraints cst env
- | SFBalias (mp,None) -> env
+ | SFBalias (mp,_,Some cst) -> Environ.add_constraints cst env
+ | SFBalias (mp,_,None) -> env
| SFBmodtype mtb -> add_modtype_constraints env mtb
and add_module_constraints env mb =
@@ -352,15 +399,15 @@ let rec struct_expr_constraints cst = function
| SEBwith(meb,With_definition_body(_,cb))->
struct_expr_constraints
(Univ.Constraint.union cb.const_constraints cst) meb
- | SEBwith(meb,With_module_body(_,_,cst1))->
+ | SEBwith(meb,With_module_body(_,_,_,cst1))->
struct_expr_constraints (Univ.Constraint.union cst1 cst) meb
and struct_elem_constraints cst = function
| SFBconst cb -> cst
| SFBmind mib -> cst
| SFBmodule mb -> module_constraints cst mb
- | SFBalias (mp,Some cst1) -> Univ.Constraint.union cst1 cst
- | SFBalias (mp,None) -> cst
+ | SFBalias (mp,_,Some cst1) -> Univ.Constraint.union cst1 cst
+ | SFBalias (mp,_,None) -> cst
| SFBmodtype mtb -> modtype_constraints cst mtb
and module_constraints cst mb =
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 7bed3254..25a11c69 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modops.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: modops.ml 11514 2008-10-28 13:39:02Z soubiran $ i*)
(*i*)
open Util
@@ -113,16 +113,18 @@ let module_body_of_type mtb =
mod_retroknowledge = []}
let module_type_of_module mp mb =
- {typ_expr =
+ let mp1,expr =
(match mb.mod_type with
- | Some expr -> expr
+ | Some expr -> mp,expr
| None -> (match mb.mod_expr with
- | Some expr -> expr
+ | Some (SEBident mp') ->(Some mp'),(SEBident mp')
+ | Some expr -> mp,expr
| None ->
- anomaly "Modops: empty expr and type"));
- typ_alias = mb.mod_alias;
- typ_strength = mp
- }
+ anomaly "Modops: empty expr and type")) in
+ {typ_expr = expr;
+ typ_alias = mb.mod_alias;
+ typ_strength = mp1
+ }
let rec check_modpath_equiv env mp1 mp2 =
if mp1=mp2 then () else
@@ -132,13 +134,14 @@ let rec check_modpath_equiv env mp1 mp2 =
else
error_not_equal mp1 mp2
-let subst_with_body sub = function
- | With_module_body(id,mp,cst) ->
- With_module_body(id,subst_mp sub mp,cst)
+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_definition_body(id,cb) ->
With_definition_body( id,subst_const_body sub cb)
-let rec 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
@@ -156,8 +159,9 @@ and subst_structure sub sign =
SFBmodule (subst_module sub mb)
| SFBmodtype mtb ->
SFBmodtype (subst_modtype sub mtb)
- | SFBalias (mp,cst) ->
- SFBalias (subst_mp sub mp,cst)
+ | 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
@@ -277,7 +281,7 @@ let rec eval_struct env = function
| SEBwith (mtb,(With_definition_body _ as wdb)) ->
let mtb',_ = merge_with env mtb wdb empty_subst in
mtb'
- | SEBwith (mtb, (With_module_body (_,mp,_) as wdb)) ->
+ | SEBwith (mtb, (With_module_body (_,mp,_,_) as wdb)) ->
let alias_in_mp =
(lookup_modtype mp env).typ_alias in
let alias_in_mp = match eval_struct env (SEBident mp) with
@@ -303,8 +307,8 @@ and merge_with env mtb with_decl alias=
| _ -> 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
+ | 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
@@ -314,47 +318,54 @@ and merge_with env mtb with_decl alias=
| [] -> MPself msid
| i::r -> MPdot(mp_rec r,label_of_id i)
in
+ let env' = add_signature (MPself msid) before env in
let new_spec,subst = match with_decl with
| With_definition_body ([],_)
- | With_module_body ([],_,_) -> assert false
+ | With_module_body ([],_,_,_) -> assert false
| With_definition_body ([id],c) ->
SFBconst c,None
- | With_module_body ([id], mp,cst) ->
- let mp' = scrape_alias mp env in
+ | With_module_body ([id], mp,typ_opt,cst) ->
+ let mp' = scrape_alias mp env' in
let new_alias = update_subst alias (map_mp (mp_rec [id]) mp') in
- SFBalias (mp,Some cst),
+ SFBalias (mp,typ_opt,Some cst),
Some(join (map_mp (mp_rec [id]) mp') new_alias)
| With_definition_body (_::_,_)
- | With_module_body (_::_,_,_) ->
- let old = match spec with
- SFBmodule msb -> msb
+ | With_module_body (_::_,_,_,_) ->
+ let old,aliasold = match spec with
+ SFBmodule msb -> Some msb, None
+ | SFBalias (mpold,typ_opt,cst) ->None, Some (mpold,typ_opt,cst)
| _ -> error_not_a_module (string_of_label 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,cst) ->
- let mp' = scrape_alias mp env in
- With_module_body (idl,mp,cst),
- Some(map_mp (mp_rec (List.rev idc)) mp')
- in
- let subst = match subst1 with
- | None -> None
- | Some s -> Some (join s (update_subst alias s)) in
- let modtype,subst_msb =
- 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 = begin
- match subst_msb with
- |None -> empty_subst
- |Some s -> s
- end;
- mod_retroknowledge = old.mod_retroknowledge}
- in
- (SFBmodule msb),subst
+ if aliasold = None then
+ let old = Option.get old 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,typ_opt,cst) ->
+ let mp' = scrape_alias mp env' in
+ With_module_body (idl,mp,typ_opt,cst),
+ Some(map_mp (mp_rec (List.rev idc)) mp')
+ in
+ let subst = match subst1 with
+ | None -> None
+ | Some s -> Some (join s (update_subst alias s)) in
+ let modtype,subst_msb =
+ 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 = begin
+ match subst_msb with
+ |None -> empty_subst
+ |Some s -> s
+ end;
+ mod_retroknowledge = old.mod_retroknowledge}
+ in
+ (SFBmodule msb),subst
+ else
+ let mpold,typ_opt,cst = Option.get aliasold in
+ SFBalias (mpold,typ_opt,cst),None
in
SEBstruct(msid, before@(l,new_spec)::
(Option.fold_right subst_structure subst after)),subst
@@ -371,7 +382,7 @@ and add_signature mp sign env =
| SFBmodule mb ->
add_module (MPdot (mp,l)) mb env
(* adds components as well *)
- | SFBalias (mp1,cst) ->
+ | SFBalias (mp1,_,cst) ->
Environ.register_alias (MPdot(mp,l)) mp1 env
| SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l))
mtb env
@@ -402,7 +413,7 @@ and constants_of_specification env mp sign =
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) ->
+ | SFBalias (mp1,typ_opt,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
@@ -494,7 +505,7 @@ and strengthen_sig env msid sign mp = match sign with
(MPdot (MPself msid,l)) mb env in
let rest' = strengthen_sig env' msid rest mp in
item':: rest'
- | ((l,SFBalias (mp1,cst)) as item) :: rest ->
+ | ((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'
diff --git a/kernel/names.ml b/kernel/names.ml
index 25f03495..b4dcd7c8 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: names.ml 11238 2008-07-19 09:34:03Z herbelin $ *)
+(* $Id: names.ml 11750 2009-01-05 20:47:34Z herbelin $ *)
open Pp
open Util
@@ -17,7 +17,7 @@ type identifier = string
let id_ord = Pervasives.compare
-let id_of_string s = check_ident s; String.copy s
+let id_of_string s = check_ident_soft s; String.copy s
let string_of_id id = String.copy id
@@ -86,6 +86,7 @@ type label = string
type mod_self_id = uniq_ident
let make_msid = make_uid
+let repr_msid (n, id, dp) = (n, id, dp)
let debug_string_of_msid = debug_string_of_uid
let refresh_msid (_,s,dir) = make_uid dir s
let string_of_msid = string_of_uid
@@ -94,6 +95,7 @@ let label_of_msid (_,s,_) = s
type mod_bound_id = uniq_ident
let make_mbid = make_uid
+let repr_mbid (n, id, dp) = (n, id, dp)
let debug_string_of_mbid = debug_string_of_uid
let string_of_mbid = string_of_uid
let id_of_mbid (_,s,_) = s
@@ -115,8 +117,14 @@ type module_path =
| MPself of mod_self_id
| MPdot of module_path * label
+
+let rec check_bound_mp = function
+ | MPbound _ -> true
+ | MPdot(mp,_) ->check_bound_mp mp
+ | _ -> false
+
let rec string_of_mp = function
- | MPfile sl -> string_of_dirpath sl
+ | MPfile sl -> "MPfile (" ^ string_of_dirpath sl ^ ")"
| MPbound uid -> string_of_uid uid
| MPself uid -> string_of_uid uid
| MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
diff --git a/kernel/names.mli b/kernel/names.mli
index c6f59048..49b10bfe 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: names.mli 10919 2008-05-11 22:04:26Z msozeau $ i*)
+(*i $Id: names.mli 11582 2008-11-12 19:49:57Z notin $ i*)
(*s Identifiers *)
@@ -48,6 +48,7 @@ type mod_self_id
(* The first argument is a file name - to prevent conflict between
different files *)
val make_msid : dir_path -> string -> mod_self_id
+val repr_msid : mod_self_id -> int * string * dir_path
val id_of_msid : mod_self_id -> identifier
val label_of_msid : mod_self_id -> label
val refresh_msid : mod_self_id -> mod_self_id
@@ -58,6 +59,7 @@ val string_of_msid : mod_self_id -> string
type mod_bound_id
val make_mbid : dir_path -> string -> mod_bound_id
+val repr_mbid : mod_bound_id -> int * string * dir_path
val id_of_mbid : mod_bound_id -> identifier
val label_of_mbid : mod_bound_id -> label
val debug_string_of_mbid : mod_bound_id -> string
@@ -82,6 +84,7 @@ type module_path =
| MPdot of module_path * label
(*i | MPapply of module_path * module_path in the future (maybe) i*)
+val check_bound_mp : module_path -> bool
val string_of_mp : module_path -> string
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 3c7461b2..fbb05a2d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: safe_typing.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: safe_typing.ml 11453 2008-10-15 14:42:34Z soubiran $ *)
open Util
open Names
@@ -312,6 +312,13 @@ let add_alias l mp senv =
check_label l senv.labset;
let mp' = MPdot(senv.modinfo.modpath, l) in
let mp1 = scrape_alias mp senv.env in
+ let typ_opt =
+ if check_bound_mp mp then
+ Some (strengthen senv.env
+ (lookup_modtype mp senv.env).typ_expr mp)
+ else
+ None
+ in
(* we get all updated alias substitution {mp1.K\M} that comes from mp1 *)
let _,sub = Modops.update_subst senv.env (lookup_module mp1 senv.env) mp1 in
(* transformation of {mp1.K\M} to {mp.K\M}*)
@@ -327,7 +334,7 @@ let add_alias l mp senv =
alias_subst = join
senv.modinfo.alias_subst sub};
labset = Labset.add l senv.labset;
- revstruct = (l,SFBalias (mp,None))::senv.revstruct;
+ revstruct = (l,SFBalias (mp,typ_opt,None))::senv.revstruct;
univ = senv.univ;
engagement = senv.engagement;
imports = senv.imports;
@@ -502,7 +509,7 @@ let end_module l restype senv =
imports = senv'.imports;
loads = senv'.loads;
local_retroknowledge = senv'.local_retroknowledge }
- | SFBalias (mp',cst) ->
+ | SFBalias (mp',typ_opt,cst) ->
let env' = Option.fold_right
Environ.add_constraints cst senv.env in
let mp = MPdot(senv.modinfo.modpath, l) in
@@ -518,7 +525,7 @@ let end_module l restype senv =
alias_subst = join
senv.modinfo.alias_subst sub};
labset = Labset.add l senv.labset;
- revstruct = (l,SFBalias (mp',cst))::senv.revstruct;
+ revstruct = (l,SFBalias (mp',typ_opt,cst))::senv.revstruct;
univ = senv.univ;
engagement = senv.engagement;
imports = senv.imports;
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 14020c0b..98ee1dbb 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtyping.ml 11142 2008-06-18 15:37:31Z soubiran $ i*)
+(*i $Id: subtyping.ml 11453 2008-10-15 14:42:34Z soubiran $ i*)
(*i*)
open Util
@@ -33,7 +33,7 @@ type namedobject =
| IndConstr of constructor * mutual_inductive_body
| Module of module_body
| Modtype of module_type_body
- | Alias of module_path
+ | Alias of module_path * struct_expr_body option
(* adds above information about one mutual inductive: all types and
constructors *)
@@ -64,7 +64,7 @@ let make_label_map mp list =
add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map
| SFBmodule mb -> add_map (Module mb)
| SFBmodtype mtb -> add_map (Modtype mtb)
- | SFBalias (mp,cst) -> add_map (Alias mp)
+ | SFBalias (mp,typ_opt,cst) -> add_map (Alias (mp,typ_opt))
in
List.fold_right add_one list Labmap.empty
@@ -352,23 +352,23 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') =
begin
match info1 with
| Module msb -> check_modules cst env msid1 l msb msb2 alias
- | Alias mp ->let msb =
+ | Alias (mp,typ_opt) ->let msb =
{mod_expr = Some (SEBident mp);
- mod_type = Some (eval_struct env (SEBident mp));
+ mod_type = typ_opt;
mod_constraints = Constraint.empty;
mod_alias = (lookup_modtype mp env).typ_alias;
mod_retroknowledge = []} in
check_modules cst env msid1 l msb msb2 alias
| _ -> error_not_match l spec2
end
- | SFBalias (mp,_) ->
+ | SFBalias (mp,typ_opt,_) ->
begin
match info1 with
- | Alias mp1 -> check_modpath_equiv env mp mp1; cst
+ | Alias (mp1,_) -> check_modpath_equiv env mp mp1; cst
| Module msb ->
let msb1 =
{mod_expr = Some (SEBident mp);
- mod_type = Some (eval_struct env (SEBident mp));
+ mod_type = typ_opt;
mod_constraints = Constraint.empty;
mod_alias = (lookup_modtype mp env).typ_alias;
mod_retroknowledge = []} in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 11a5452c..3d254ce6 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: univ.ml 11301 2008-08-04 19:41:18Z herbelin $ *)
+(* $Id: univ.ml 11596 2008-11-16 15:34:06Z letouzey $ *)
(* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
(* Extension with algebraic universes by HH [Sep 2001] *)
@@ -43,13 +43,25 @@ type universe_level =
| Set
| Level of Names.dir_path * int
+(* A specialized comparison function: we compare the [int] part first.
+ This way, most of the time, the [dir_path] part is not considered. *)
+
+let cmp_univ_level u v = match u,v with
+ | Set, Set -> 0
+ | Set, _ -> -1
+ | _, Set -> 1
+ | Level (dp1,i1), Level (dp2,i2) ->
+ if i1 < i2 then -1
+ else if i1 > i2 then 1
+ else compare dp1 dp2
+
type universe =
| Atom of universe_level
| Max of universe_level list * universe_level list
module UniverseOrdered = struct
type t = universe_level
- let compare = Pervasives.compare
+ let compare = cmp_univ_level
end
let string_of_univ_level = function
@@ -86,7 +98,8 @@ let super = function
Used to type the products. *)
let sup u v =
match u,v with
- | Atom u, Atom v -> if u = v then Atom u else Max ([u;v],[])
+ | Atom u, Atom v ->
+ if cmp_univ_level u v = 0 then Atom u else Max ([u;v],[])
| u, Max ([],[]) -> u
| Max ([],[]), v -> v
| Atom u, Max (gel,gtl) -> Max (list_add_set u gel,gtl)
@@ -601,12 +614,12 @@ let dump_universes output g =
let u_str = string_of_univ_level u in
List.iter
(fun v ->
- Printf.fprintf output "%s > %s ;\n" u_str
+ Printf.fprintf output "%s < %s ;\n" u_str
(string_of_univ_level v))
lt;
List.iter
(fun v ->
- Printf.fprintf output "%s >= %s ;\n" u_str
+ Printf.fprintf output "%s <= %s ;\n" u_str
(string_of_univ_level v))
le
| Equiv (u,v) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-26 07:33:37 +0000