From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- library/lib.ml | 239 +++++++++++++++++++++------------------------------------ 1 file changed, 87 insertions(+), 152 deletions(-) (limited to 'library/lib.ml') diff --git a/library/lib.ml b/library/lib.ml index 6f8655d3..7554fd0b 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -1,26 +1,26 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* f i (make_oname prefix id, obj)) @@ -69,10 +72,9 @@ let classify_segment seg = (* LEM; TODO: Understand what this does and see if what I do is the correct thing for ClosedMod(ule|type) *) | (_,ClosedModule _) :: stk -> clean acc stk - | (_,ClosedModtype _) :: stk -> clean acc stk | (_,OpenedSection _) :: _ -> error "there are still opened sections" - | (_,OpenedModule _) :: _ -> error "there are still opened modules" - | (_,OpenedModtype _) :: _ -> error "there are still opened module types" + | (_,OpenedModule (ty,_,_,_)) :: _ -> + error ("there are still opened " ^ module_kind ty ^"s") | (_,FrozenState _) :: stk -> clean acc stk in clean ([],[],[]) (List.rev seg) @@ -144,8 +146,7 @@ let make_oname id = make_path id, make_kn id let recalc_path_prefix () = let rec recalc = function | (sp, OpenedSection (dir,_)) :: _ -> dir - | (sp, OpenedModule (_,dir,_)) :: _ -> dir - | (sp, OpenedModtype (dir,_)) :: _ -> dir + | (sp, OpenedModule (_,_,dir,_)) :: _ -> dir | (sp, CompilingLibrary dir) :: _ -> dir | _::l -> recalc l | [] -> initial_prefix @@ -181,7 +182,6 @@ let split_lib_gen test = then Some (collect after [hd] before) else (match hd with | (sp,ClosedModule seg) - | (sp,ClosedModtype seg) | (sp,ClosedSection seg) -> (match findeq after seg with | None -> findeq (hd::after) before @@ -197,11 +197,11 @@ let split_lib_gen test = let split_lib sp = split_lib_gen (fun x -> fst x = sp) let split_lib_at_opening sp = - let a,s,b = split_lib_gen (function - | x,(OpenedSection _|OpenedModule _|OpenedModtype _|CompilingLibrary _) -> - x = sp - | _ -> - false) in + let is_sp = function + | x,(OpenedSection _|OpenedModule _|CompilingLibrary _) -> x = sp + | _ -> false + in + let a,s,b = split_lib_gen is_sp in assert (List.tl s = []); (a,List.hd s,b) @@ -254,97 +254,66 @@ let add_frozen_state () = (* Modules. *) - -let is_opened id = function - oname,(OpenedSection _ | OpenedModule _ | OpenedModtype _) when - basename (fst oname) = id -> true - | _ -> false - let is_opening_node = function - _,(OpenedSection _ | OpenedModule _ | OpenedModtype _) -> true + | _,(OpenedSection _ | OpenedModule _) -> true | _ -> false +let is_opening_node_or_lib = function + | _,(CompilingLibrary _ | OpenedSection _ | OpenedModule _) -> true + | _ -> false let current_mod_id () = - try match find_entry_p is_opening_node with - | oname,OpenedModule (_,_,fs) -> - basename (fst oname) - | oname,OpenedModtype (_,fs) -> - basename (fst oname) + try match find_entry_p is_opening_node_or_lib with + | oname,OpenedModule (_,_,_,fs) -> basename (fst oname) + | oname,CompilingLibrary _ -> basename (fst oname) | _ -> error "you are not in a module" - with Not_found -> - error "no opened modules" + with Not_found -> error "no opened modules" -let start_module export id mp fs = +let start_mod is_type export id mp fs = let dir = add_dirpath_suffix (fst !path_prefix) id in let prefix = dir,(mp,Names.empty_dirpath) in - let oname = make_path id, make_kn id in - if Nametab.exists_module dir then - errorlabstrm "open_module" (pr_id id ++ str " already exists") ; - add_entry oname (OpenedModule (export,prefix,fs)); + let sp = make_path id in + let oname = sp, make_kn id in + let exists = + if is_type then Nametab.exists_cci sp else Nametab.exists_module dir + in + if exists then + errorlabstrm "open_module" (pr_id id ++ str " already exists"); + add_entry oname (OpenedModule (is_type,export,prefix,fs)); path_prefix := prefix; prefix (* add_frozen_state () must be called in declaremods *) +let start_module = start_mod false +let start_modtype = start_mod true None + let error_still_opened string oname = let id = basename (fst oname) in - errorlabstrm "" (str string ++ spc () ++ pr_id id ++ str " is still opened.") + errorlabstrm "" + (str ("The "^string^" ") ++ pr_id id ++ str " is still opened.") -let end_module () = +let end_mod is_type = let oname,fs = try match find_entry_p is_opening_node with - | oname,OpenedModule (_,_,fs) -> oname,fs - | oname,OpenedModtype _ -> error_still_opened "Module Type" oname - | oname,OpenedSection _ -> error_still_opened "Section" oname + | oname,OpenedModule (ty,_,_,fs) -> + if ty = is_type then oname,fs + else error_still_opened (module_kind ty) oname + | oname,OpenedSection _ -> error_still_opened "section" oname | _ -> assert false - with Not_found -> - error "No opened modules." + with Not_found -> error "No opened modules." in let (after,mark,before) = split_lib_at_opening oname in lib_stk := before; add_entry oname (ClosedModule (List.rev (mark::after))); let prefix = !path_prefix in - (* LEM: This module business seems more complicated than sections; - shouldn't a backtrack into a closed module also do something - with global.ml, given that closing a module does? - TODO - *) recalc_path_prefix (); (* add_frozen_state must be called after processing the module, because we cannot recache interactive modules *) (oname, prefix, fs, after) -let start_modtype id mp fs = - let dir = add_dirpath_suffix (fst !path_prefix) id in - let prefix = dir,(mp,Names.empty_dirpath) in - let sp = make_path id in - let name = sp, make_kn id in - if Nametab.exists_cci sp then - errorlabstrm "open_modtype" (pr_id id ++ str " already exists") ; - add_entry name (OpenedModtype (prefix,fs)); - path_prefix := prefix; - prefix - -let end_modtype () = - let oname,fs = - try match find_entry_p is_opening_node with - | oname,OpenedModtype (_,fs) -> oname,fs - | oname,OpenedModule _ -> error_still_opened "Module" oname - | oname,OpenedSection _ -> error_still_opened "Section" oname - | _ -> assert false - with Not_found -> - error "no opened module types" - in - let (after,mark,before) = split_lib_at_opening oname in - lib_stk := before; - add_entry oname (ClosedModtype (List.rev (mark::after))); - let dir = !path_prefix in - recalc_path_prefix (); - (* add_frozen_state must be called after processing the module type. - This is because we cannot recache interactive module types *) - (oname,dir,fs,after) - +let end_module () = end_mod false +let end_modtype () = end_mod true let contents_after = function | None -> !lib_stk @@ -352,13 +321,6 @@ let contents_after = function (* Modules. *) -let check_for_comp_unit () = - let is_decl = function (_,FrozenState _) -> false | _ -> true in - try - let _ = find_entry_p is_decl in - error "a module cannot be started after some declarations" - with Not_found -> () - (* TODO: use check_for_module ? *) let start_compilation s mp = if !comp_name <> None then @@ -374,21 +336,18 @@ let end_compilation dir = let _ = try match snd (find_entry_p is_opening_node) with | OpenedSection _ -> error "There are some open sections." - | OpenedModule _ -> error "There are some open modules." - | OpenedModtype _ -> error "There are some open module types." + | OpenedModule (ty,_,_,_) -> + error ("There are some open "^module_kind ty^"s.") | _ -> assert false - with - Not_found -> () + with Not_found -> () in - let module_p = - function (_,CompilingLibrary _) -> true | x -> is_opening_node x + let is_opening_lib = function _,CompilingLibrary _ -> true | _ -> false in let oname = - try match find_entry_p module_p with - (oname, CompilingLibrary prefix) -> oname + try match find_entry_p is_opening_lib with + | (oname, CompilingLibrary prefix) -> oname | _ -> assert false - with - Not_found -> anomaly "No module declared" + with Not_found -> anomaly "No module declared" in let _ = match !comp_name with @@ -399,31 +358,23 @@ let end_compilation dir = " and not " ^ (Names.string_of_dirpath m)); in let (after,mark,before) = split_lib_at_opening oname in - comp_name := None; - !path_prefix,after + comp_name := None; + !path_prefix,after -(* Returns true if we are inside an opened module type *) -let is_modtype () = - let opened_p = function - | _, OpenedModtype _ -> true - | _ -> false - in - try - let _ = find_entry_p opened_p in true - with - Not_found -> false - -(* Returns true if we are inside an opened module *) -let is_module () = - let opened_p = function - | _, OpenedModule _ -> true +(* Returns true if we are inside an opened module or module type *) + +let is_module_gen which = + let test = function + | _, OpenedModule (ty,_,_,_) -> which ty | _ -> false in - try - let _ = find_entry_p opened_p in true - with - Not_found -> false + try + let _ = find_entry_p test in true + with Not_found -> false +let is_module_or_modtype () = is_module_gen (fun _ -> true) +let is_modtype () = is_module_gen (fun b -> b) +let is_module () = is_module_gen (fun b -> not b) (* Returns the opening node of a given name *) let find_opening_node id = @@ -495,8 +446,6 @@ let add_section_constant kn = let replacement_context () = pi2 (List.hd !sectab) -let variables_context () = pi1 (List.hd !sectab) - let section_segment_of_constant con = Names.Cmap.find con (fst (pi3 (List.hd !sectab))) @@ -563,8 +512,8 @@ let discharge_item ((sp,_ as oname),e) = | Leaf lobj -> Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) | FrozenState _ -> None - | ClosedSection _ | ClosedModtype _ | ClosedModule _ -> None - | OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ -> + | ClosedSection _ | ClosedModule _ -> None + | OpenedSection _ | OpenedModule _ | CompilingLibrary _ -> anomaly "discharge_item" let close_section () = @@ -590,8 +539,8 @@ let close_section () = (*****************) (* Backtracking. *) -let (inLabel,outLabel) = - declare_object {(default_object "DOT") with +let (inLabel : int -> obj), (outLabel : obj -> int) = + declare_object_full {(default_object "DOT") with classify_function = (fun _ -> Dispose)} let recache_decl = function @@ -604,13 +553,6 @@ let recache_context ctx = let is_frozen_state = function (_,FrozenState _) -> true | _ -> false -let has_top_frozen_state () = - let rec aux = function - | (sp, FrozenState _)::_ -> Some sp - | (sp, Leaf o)::t when object_tag o = "DOT" -> aux t - | _ -> None - in aux !lib_stk - let set_lib_stk new_lib_stk = lib_stk := new_lib_stk; recalc_path_prefix (); @@ -630,17 +572,9 @@ let reset_to_gen test = let reset_to sp = reset_to_gen (fun x -> fst x = sp) -let reset_to_state sp = - let (_,eq,before) = split_lib sp in - (* if eq a frozen state, we'll reset to it *) - match eq with - | [_,FrozenState f] -> lib_stk := eq@before; recalc_path_prefix (); unfreeze_summaries f - | _ -> error "Not a frozen state" - - (* LEM: TODO * We will need to muck with frozen states in after, too! - * Not only FrozenState, but also those embedded in Opened(Section|Module|Modtype) + * Not only FrozenState, but also those embedded in Opened(Section|Module) *) let delete_gen test = let (after,equal,before) = split_lib_gen test in @@ -676,8 +610,8 @@ let remove_name (loc,id) = delete sp let is_mod_node = function - | OpenedModule _ | OpenedModtype _ | OpenedSection _ - | ClosedModule _ | ClosedModtype _ | ClosedSection _ -> true + | OpenedModule _ | OpenedSection _ + | ClosedModule _ | ClosedSection _ -> true | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" || t = "MODULE ALIAS" | _ -> false @@ -710,17 +644,16 @@ let is_label_n n x = | (sp,Leaf o) when object_tag o = "DOT" && n = outLabel o -> true | _ -> false -(* Reset the label registered by [mark_end_of_command()] with number n. *) +(** Reset the label registered by [mark_end_of_command()] with number n, + which should be strictly in the past. *) + let reset_label n = - let current = current_command_label() in - if n < current then - let res = reset_to_gen (is_label_n n) in - set_command_label (n-1); (* forget state numbers after n only if reset succeeded *) - res - else (* optimisation to avoid recaching when not necessary (why is it so long??) *) - match !lib_stk with - | [] -> () - | x :: ls -> (lib_stk := ls;set_command_label (n-1)) + if n >= current_command_label () then + error "Cannot backtrack to the current label or a future one"; + let res = reset_to_gen (is_label_n n) in + (* forget state numbers after n only if reset succeeded *) + set_command_label (n-1); + res let rec back_stk n stk = match stk with @@ -729,7 +662,9 @@ let rec back_stk n stk = | _::tail -> back_stk n tail | [] -> error "Reached begin of command history" -let back n = reset_to (back_stk n !lib_stk) +let back n = + reset_to (back_stk n !lib_stk); + set_command_label (current_command_label () - n - 1) (* State and initialization. *) @@ -793,7 +728,7 @@ let rec split_mp mp = | Names.MPdot (prfx, lbl) -> let mprec, dprec = split_mp prfx in mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec)) - | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.make_dirpath [Names.id_of_string id] + | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in library_dp(), Names.make_dirpath [id] let split_modpath mp = let rec aux = function -- cgit v1.2.3