From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- checker/check.ml | 4 ++-- checker/checker.ml | 13 +++++-------- checker/declarations.ml | 18 ++++++++++-------- checker/declarations.mli | 6 ++++-- checker/mod_checking.ml | 26 +++++++++++++------------- checker/modops.ml | 24 ++++++++++++------------ checker/subtyping.ml | 14 +++++++------- 7 files changed, 53 insertions(+), 52 deletions(-) (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index 40ac604e..82df62b4 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -211,7 +211,7 @@ let locate_absolute_library dir = if loadpath = [] then raise LibUnmappedDir; try let name = string_of_id base^".vo" in - let _, file = System.where_in_path false loadpath name in + let _, file = System.where_in_path ~warn:false loadpath name in (dir, file) with Not_found -> (* Last chance, removed from the file system but still in memory *) @@ -231,7 +231,7 @@ let locate_qualified_library qid = in if loadpath = [] then raise LibUnmappedDir; let name = qid.basename^".vo" in - let path, file = System.where_in_path true loadpath name in + let path, file = System.where_in_path loadpath name in let dir = extend_dirpath (find_logical_path path) (id_of_string qid.basename) in (* Look if loaded *) diff --git a/checker/checker.ml b/checker/checker.ml index 1ed094cf..3d928933 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -43,7 +43,8 @@ let (/) = Filename.concat let get_version_date () = try - let ch = open_in (Coq_config.coqlib^"/revision") in + let coqlib = Envars.coqlib () in + let ch = open_in (Filename.concat coqlib "revision") in let ver = input_line ch in let rev = input_line ch in (ver,rev) @@ -108,13 +109,9 @@ let set_rec_include d p = check_coq_overwriting p; push_rec_include(d,p) -(* Initializes the LoadPath according to COQLIB and Coq_config *) +(* Initializes the LoadPath *) let init_load_path () = - let coqlib = - (* variable COQLIB overrides the default library *) - getenv_else "COQLIB" - (if Coq_config.local || !Flags.boot then Coq_config.coqtop - else Coq_config.coqlib) in + let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in let contrib = coqlib/"contrib" in (* first user-contrib *) @@ -323,7 +320,7 @@ let parse_args() = | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0 + print_endline (Envars.coqlib ()); exit 0 | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () diff --git a/checker/declarations.ml b/checker/declarations.ml index 71b6c9ca..2cf3854a 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -562,7 +562,7 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * Univ.constraints option + | SFBalias of module_path * struct_expr_body option * Univ.constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list @@ -576,7 +576,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 * Univ.constraints + With_module_body of identifier list * module_path * + struct_expr_body option * Univ.constraints | With_definition_body of identifier list * constant_body and module_body = @@ -592,13 +593,14 @@ and module_type_body = typ_alias : substitution} -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 @@ -616,8 +618,8 @@ 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 diff --git a/checker/declarations.mli b/checker/declarations.mli index fdea3383..78bf2053 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -150,7 +150,8 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * Univ.constraints option + | SFBalias of module_path * struct_expr_body option + * Univ.constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list @@ -164,7 +165,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 * Univ.constraints + With_module_body of identifier list * module_path * + struct_expr_body option * Univ.constraints | With_definition_body of identifier list * constant_body and module_body = diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 379273af..af5e4f46 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -145,9 +145,9 @@ and check_with_aux_def env mtb with_decl = | _ -> 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 @@ -173,8 +173,8 @@ 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,cst) -> - With_module_body (idl,c,cst) in + | 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 | Some msb -> error_a_generative_module_expected l @@ -192,9 +192,9 @@ and check_with_aux_mod env mtb with_decl = msid,msid',(subst_signature_msid msid (MPself(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,_,_) -> + | 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 @@ -206,11 +206,11 @@ and check_with_aux_mod env mtb with_decl = in let env' = Modops.add_signature (MPself msid) before env in match with_decl with - | With_module_body ([],_,_) -> assert false - | With_module_body ([id], mp,_) -> + | 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' + | SFBalias (mp',_,_) -> None,Some mp' | _ -> error_not_a_module l in let mtb' = lookup_modtype mp env' in @@ -223,7 +223,7 @@ and check_with_aux_mod env mtb with_decl = anomaly "Mod_typing:no implementation and no alias" in join (map_mp (mp_rec [id]) mp) mtb'.typ_alias - | With_module_body (_::_,mp,_) -> + | With_module_body (_::_,mp,_,_) -> let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module l @@ -234,8 +234,8 @@ 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,cst) -> - With_module_body (idl,c,cst) in + | 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 @@ -290,7 +290,7 @@ and check_structure_field (s,env) mp lab = function 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) -> + | SFBalias(mp2,_,cst) -> (* cf Safe_typing.add_alias *) (try let mp' = MPdot(mp,lab) in diff --git a/checker/modops.ml b/checker/modops.ml index f79e52c2..27ea4d55 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -145,7 +145,7 @@ let rec eval_struct env = function (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)) -> + | 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 @@ -167,8 +167,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 @@ -180,15 +180,15 @@ and merge_with env mtb with_decl alias= 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) -> + | With_module_body ([id], mp,typ_opt,cst) -> let mp' = scrape_alias mp env in - SFBalias (mp,Some cst), + SFBalias (mp,typ_opt,Some cst), Some(join (map_mp (mp_rec [id]) mp') alias) | With_definition_body (_::_,_) - | With_module_body (_::_,_,_) -> + | With_module_body (_::_,_,_,_) -> let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module l @@ -196,8 +196,8 @@ and merge_with env mtb with_decl alias= 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) -> - With_module_body (idl,mp,cst), + | 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 @@ -227,7 +227,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 @@ -257,7 +257,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,_,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 @@ -323,7 +323,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/checker/subtyping.ml b/checker/subtyping.ml index fb95b606..7a6868fe 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -32,7 +32,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 *) @@ -63,7 +63,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,t,cst) -> add_map (Alias (mp,t)) in List.fold_right add_one list Labmap.empty @@ -308,23 +308,23 @@ and check_signatures env (msid1,sig1) alias (msid2,sig2') = begin match info1 with | Module msb -> check_modules env msid1 l msb msb2 - | 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 env msid1 l msb msb2 | _ -> error_not_match l spec2 end - | SFBalias (mp,_) -> + | SFBalias (mp,typ_opt,_) -> begin match info1 with - | Alias mp1 -> check_modpath_equiv env mp mp1 + | Alias (mp1,_) -> check_modpath_equiv env mp mp1 | 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 -- cgit v1.2.3