From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 25 Jul 2008 15:12:53 +0200 Subject: Imported Upstream version 8.2~beta3+dfsg --- library/lib.ml | 233 ++++++++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 171 insertions(+), 62 deletions(-) (limited to 'library/lib.ml') diff --git a/library/lib.ml b/library/lib.ml index 4a4e90c1..ce3d2520 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: lib.ml 10269 2007-10-29 11:09:43Z notin $ *) +(* $Id: lib.ml 10982 2008-05-24 14:32:25Z herbelin $ *) open Pp open Util @@ -22,9 +22,11 @@ type node = | Leaf of obj | CompilingLibrary of object_prefix | OpenedModule of bool option * object_prefix * Summary.frozen + | ClosedModule of library_segment | OpenedModtype of object_prefix * Summary.frozen + | ClosedModtype of library_segment | OpenedSection of object_prefix * Summary.frozen - | ClosedSection + | ClosedSection of library_segment | FrozenState of Summary.frozen and library_entry = object_name * node @@ -60,7 +62,11 @@ let classify_segment seg = clean ((id,o')::substl, keepl, anticipl) stk | Anticipate o' -> clean (substl, keepl, o'::anticipl) stk) - | (oname,ClosedSection) :: stk -> clean acc stk + | (_,ClosedSection _) :: stk -> clean acc stk + (* 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" @@ -92,11 +98,15 @@ let library_dp () = module path and relative section path *) let path_prefix = ref initial_prefix - let cwd () = fst !path_prefix let make_path id = Libnames.make_path (cwd ()) id +let path_of_include () = + let dir = Names.repr_dirpath (cwd ()) in + let new_dir = List.tl dir in + let id = List.hd dir in + Libnames.make_path (Names.make_dirpath new_dir) id let current_prefix () = snd !path_prefix @@ -150,18 +160,32 @@ let find_split_p p = in find !lib_stk -let split_lib sp = +let split_lib_gen test = let rec collect after equal = function - | ((sp',_) as hd)::before -> - if sp = sp' then collect after (hd::equal) before else after,equal,hd::before - | [] -> after,equal,[] + | hd::strict_before as before -> + if test hd then collect after (hd::equal) strict_before else after,equal,before + | [] as before -> after,equal,before in let rec findeq after = function - | ((sp',_) as hd)::before -> - if sp = sp' then collect after [hd] before else findeq (hd::after) before - | [] -> error "no such entry" - in - findeq [] !lib_stk + | hd :: before -> + if test hd + 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 + | Some (sub_after,sub_equal,sub_before) -> + Some (sub_after, sub_equal, (List.append sub_before before))) + | _ -> findeq (hd::after) before) + | [] -> None + in + match findeq [] !lib_stk with + | None -> error "no such entry" + | Some r -> r + +let split_lib sp = split_lib_gen (fun x -> (fst x) = sp) (* Adding operations. *) @@ -190,9 +214,9 @@ let add_leaf id obj = add_entry oname (Leaf obj); oname -let add_discharged_leaf id obj = +let add_discharged_leaf id varinfo obj = let oname = make_oname id in - let newobj = rebuild_object obj in + let newobj = rebuild_object (varinfo, obj) in cache_object (oname,newobj); add_entry oname (Leaf newobj) @@ -216,12 +240,25 @@ let add_frozen_state () = (* Modules. *) + let is_something_opened = function (_,OpenedSection _) -> true | (_,OpenedModule _) -> true | (_,OpenedModtype _) -> true | _ -> false + +let current_mod_id () = + try match find_entry_p is_something_opened with + | oname,OpenedModule (_,_,nametab) -> + basename (fst oname) + | oname,OpenedModtype (_,nametab) -> + basename (fst oname) + | _ -> error "you are not in a module" + with Not_found -> + error "no opened modules" + + let start_module export id mp nametab = let dir = extend_dirpath (fst !path_prefix) id in let prefix = dir,(mp,empty_dirpath) in @@ -253,9 +290,15 @@ let end_module id = with Not_found -> error "no opened modules" in - let (after,_,before) = split_lib oname in + let (after,modopening,before) = split_lib oname in lib_stk := before; + add_entry (make_oname id) (ClosedModule (List.rev_append after (List.rev modopening))); 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 *) @@ -292,8 +335,9 @@ let end_modtype id = with Not_found -> error "no opened module types" in - let (after,_,before) = split_lib sp in + let (after,modtypeopening,before) = split_lib sp in lib_stk := before; + add_entry (make_oname id) (ClosedModtype (List.rev_append after (List.rev modtypeopening))); let dir = !path_prefix in recalc_path_prefix (); (* add_frozen_state must be called after processing the module type. @@ -396,18 +440,19 @@ let what_is_opened () = find_entry_p is_something_opened type abstr_list = Sign.named_context Cmap.t * Sign.named_context KNmap.t let sectab = - ref ([] : (identifier list * Cooking.work_list * abstr_list) list) + ref ([] : ((identifier * bool * Term.types option) list * Cooking.work_list * abstr_list) list) let add_section () = sectab := ([],(Cmap.empty,KNmap.empty),(Cmap.empty,KNmap.empty)) :: !sectab -let add_section_variable id = +let add_section_variable id impl keep = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) - | (vars,repl,abs)::sl -> sectab := (id::vars,repl,abs)::sl + | (vars,repl,abs)::sl -> sectab := ((id,impl,keep)::vars,repl,abs)::sl let rec extract_hyps = function - | (id::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps) + | ((id,impl,keep)::idl,(id',_,_ as d)::hyps) when id=id' -> d :: extract_hyps (idl,hyps) + | ((id,impl,Some ty)::idl,hyps) -> (id,None,ty) :: extract_hyps (idl,hyps) | (id::idl,hyps) -> extract_hyps (idl,hyps) | [], _ -> [] @@ -429,6 +474,8 @@ 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 = Cmap.find con (fst (pi3 (List.hd !sectab))) @@ -442,15 +489,15 @@ let section_instance = function | IndRef (kn,_) | ConstructRef ((kn,_),_) -> KNmap.find kn (snd (pi2 (List.hd !sectab))) -let init () = sectab := [] -let freeze () = !sectab -let unfreeze s = sectab := s +let init_sectab () = sectab := [] +let freeze_sectab () = !sectab +let unfreeze_sectab s = sectab := s let _ = Summary.declare_summary "section-context" - { Summary.freeze_function = freeze; - Summary.unfreeze_function = unfreeze; - Summary.init_function = init; + { Summary.freeze_function = freeze_sectab; + Summary.unfreeze_function = unfreeze_sectab; + Summary.init_function = init_sectab; Summary.survive_module = false; Summary.survive_section = false } @@ -476,7 +523,7 @@ let open_section id = (*Pushed for the lifetime of the section: removed by unfrozing the summary*) Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix); path_prefix := prefix; - if !Options.xml_export then !xml_open_section id; + if !Flags.xml_export then !xml_open_section id; add_section () @@ -486,9 +533,9 @@ let open_section id = let discharge_item ((sp,_ as oname),e) = match e with | Leaf lobj -> - option_map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) + Option.map (fun o -> (basename sp,o)) (discharge_object (oname,lobj)) | FrozenState _ -> None - | ClosedSection -> None + | ClosedSection _ | ClosedModtype _ | ClosedModule _ -> None | OpenedSection _ | OpenedModtype _ | OpenedModule _ | CompilingLibrary _ -> anomaly "discharge_item" @@ -504,21 +551,29 @@ let close_section id = with Not_found -> error "no opened section" in - let (secdecls,_,before) = split_lib oname in + let var_info = List.map + (fun (x, y, z) -> (x, y, match z with Some _ -> true | None -> false)) + (variables_context ()) + in + let (secdecls,secopening,before) = split_lib oname in lib_stk := before; let full_olddir = fst !path_prefix in pop_path_prefix (); - add_entry (make_oname id) ClosedSection; - if !Options.xml_export then !xml_close_section id; + add_entry (make_oname id) (ClosedSection (List.rev_append secdecls (List.rev secopening))); + if !Flags.xml_export then !xml_close_section id; let newdecls = List.map discharge_item secdecls in Summary.section_unfreeze_summaries fs; - List.iter (option_iter (fun (id,o) -> add_discharged_leaf id o)) newdecls; + List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id var_info o)) newdecls; Cooking.clear_cooking_sharing (); Nametab.push_dir (Nametab.Until 1) full_olddir (DirClosedSection full_olddir) (*****************) (* Backtracking. *) +let (inLabel,outLabel) = + declare_object {(default_object "DOT") with + classify_function = (fun _ -> Dispose)} + let recache_decl = function | (sp, Leaf o) -> cache_object (sp,o) | (_,OpenedSection _) -> add_section () @@ -529,16 +584,58 @@ let recache_context ctx = let is_frozen_state = function (_,FrozenState _) -> true | _ -> false -let reset_to sp = - let (_,_,before) = split_lib sp in - lib_stk := before; +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 (); let spf = match find_entry_p is_frozen_state with | (sp, FrozenState f) -> unfreeze_summaries f; sp | _ -> assert false in let (after,_,_) = split_lib spf in - recache_context after + try + recache_context after + with + | Not_found -> error "Tried to set environment to an incoherent state." + +let reset_to_gen test = + let (_,_,before) = split_lib_gen test in + set_lib_stk before + +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; 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) + *) +let delete_gen test = + let (after,equal,before) = split_lib_gen test in + let rec chop_at_dot = function + | [] as l -> l + | (_, Leaf o)::t when object_tag o = "DOT" -> t + | _::t -> chop_at_dot t + and chop_before_dot = function + | [] as l -> l + | (_, Leaf o)::t as l when object_tag o = "DOT" -> l + | _::t -> chop_before_dot t + in + set_lib_stk (List.rev_append (chop_at_dot after) (chop_before_dot before)) + +let delete sp = delete_gen (fun x -> (fst x) = sp) let reset_name (loc,id) = let (sp,_) = @@ -549,10 +646,20 @@ let reset_name (loc,id) = in reset_to sp +let remove_name (loc,id) = + let (sp,_) = + try + find_entry_p (fun (sp,_) -> let (_,spi) = repr_path (fst sp) in id = spi) + with Not_found -> + user_err_loc (loc,"remove_name",pr_id id ++ str ": no such entry") + in + delete sp + let is_mod_node = function | OpenedModule _ | OpenedModtype _ | OpenedSection _ - | ClosedSection -> true - | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" + | ClosedModule _ | ClosedModtype _ | ClosedSection _ -> true + | Leaf o -> let t = object_tag o in t = "MODULE" || t = "MODULE TYPE" + || t = "MODULE ALIAS" | _ -> false (* Reset on a module or section name in order to bypass constants with @@ -567,19 +674,7 @@ let reset_mod (loc,id) = with Not_found -> user_err_loc (loc,"reset_mod",pr_id id ++ str ": no such entry") in - lib_stk := before; - recalc_path_prefix (); - let spf = match find_entry_p is_frozen_state with - | (sp, FrozenState f) -> unfreeze_summaries f; sp - | _ -> assert false - in - let (after,_,_) = split_lib spf in - recache_context after - - -let (inLabel,outLabel) = - declare_object {(default_object "DOT") with - classify_function = (fun _ -> Dispose)} + set_lib_stk before let mark_end_of_command, current_command_label, set_command_label = let n = ref 0 in @@ -590,17 +685,23 @@ let mark_end_of_command, current_command_label, set_command_label = (fun () -> !n), (fun x -> n:=x) -let rec reset_label_stk n stk = - match stk with - (sp,Leaf o)::tail when object_tag o = "DOT" && n = outLabel o -> sp - | _::tail -> reset_label_stk n tail - | [] -> error "Unknown state number" +let is_label_n n x = + match x with + | (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. *) let reset_label n = - let res = reset_label_stk n !lib_stk in - set_command_label (n-1); (* forget state numbers after n only if reset succeeded *) - reset_to res - + 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)) + let rec back_stk n stk = match stk with (sp,Leaf o)::tail when object_tag o = "DOT" -> @@ -688,6 +789,14 @@ let remove_section_part ref = (************************) (* Discharging names *) +let pop_kn kn = + let (mp,dir,l) = Names.repr_kn kn in + Names.make_kn mp (dirpath_prefix dir) l + +let pop_con con = + let (mp,dir,l) = Names.repr_con con in + Names.make_con mp (dirpath_prefix dir) l + let con_defined_in_sec kn = let _,dir,_ = repr_con kn in dir <> empty_dirpath && fst (split_dirpath dir) = snd (current_prefix ()) -- cgit v1.2.3