From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- library/lib.ml | 52 +++++++++++++++++++++++++++++++++++++--------------- 1 file changed, 37 insertions(+), 15 deletions(-) (limited to 'library/lib.ml') diff --git a/library/lib.ml b/library/lib.ml index 9977b666..297441e6 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -75,7 +75,8 @@ let classify_segment seg = | (_,ClosedModule _) :: stk -> clean acc stk | (_,OpenedSection _) :: _ -> error "there are still opened sections" | (_,OpenedModule (ty,_,_,_)) :: _ -> - error ("there are still opened " ^ module_kind ty ^"s") + errorlabstrm "Lib.classify_segment" + (str "there are still opened " ++ str (module_kind ty) ++ str "s") | (_,FrozenState _) :: stk -> clean acc stk in clean ([],[],[]) (List.rev seg) @@ -197,6 +198,9 @@ let split_lib_at_opening sp = let add_entry sp node = lib_stk := (sp,node) :: !lib_stk +let pull_to_head oname = + lib_stk := (oname,List.assoc oname !lib_stk) :: List.remove_assoc oname !lib_stk + let anonymous_id = let n = ref 0 in fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n)) @@ -274,7 +278,7 @@ let start_modtype = start_mod true None let error_still_opened string oname = let id = basename (fst oname) in errorlabstrm "" - (str ("The "^string^" ") ++ pr_id id ++ str " is still opened.") + (str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.") let end_mod is_type = let oname,fs = @@ -318,7 +322,8 @@ let end_compilation_checks dir = try match snd (find_entry_p is_opening_node) with | OpenedSection _ -> error "There are some open sections." | OpenedModule (ty,_,_,_) -> - error ("There are some open "^module_kind ty^"s.") + errorlabstrm "Lib.end_compilation_checks" + (str "There are some open " ++ str (module_kind ty) ++ str "s.") | _ -> assert false with Not_found -> () in @@ -369,7 +374,8 @@ let find_opening_node id = let oname,entry = find_entry_p is_opening_node in let id' = basename (fst oname) in if not (Names.Id.equal id id') then - error ("Last block to end has name "^(Names.Id.to_string id')^"."); + errorlabstrm "Lib.find_opening_node" + (str "Last block to end has name " ++ pr_id id' ++ str "."); entry with Not_found -> error "There is nothing to end." @@ -389,10 +395,13 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.UContext.t type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t +type secentry = + | Variable of (Names.Id.t * Decl_kinds.binding_kind * + Decl_kinds.polymorphic * Univ.universe_context_set) + | Context of Univ.universe_context_set + let sectab = - Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind * - Decl_kinds.polymorphic * Univ.universe_context_set) list * - Opaqueproof.work_list * abstr_list) list) + Summary.ref ([] : (secentry list * Opaqueproof.work_list * abstr_list) list) ~name:"section-context" let add_section () = @@ -403,16 +412,25 @@ let add_section_variable id impl poly ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - sectab := ((id,impl,poly,ctx)::vars,repl,abs)::sl + sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl + +let add_section_context ctx = + match !sectab with + | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) + | (vars,repl,abs)::sl -> + sectab := (Context ctx :: vars,repl,abs)::sl let extract_hyps (secs,ohyps) = let rec aux = function - | ((id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> + | (Variable (id,impl,poly,ctx)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> let l, r = aux (idl,hyps) in (id',impl,b,t) :: l, if poly then Univ.ContextSet.union r ctx else r - | ((_,_,poly,ctx)::idl,hyps) -> + | (Variable (_,_,poly,ctx)::idl,hyps) -> let l, r = aux (idl,hyps) in l, if poly then Univ.ContextSet.union r ctx else r + | (Context ctx :: idl, hyps) -> + let l, r = aux (idl, hyps) in + l, Univ.ContextSet.union r ctx | [], _ -> [],Univ.ContextSet.empty in aux (secs,ohyps) @@ -433,7 +451,8 @@ let add_section_replacement f g hyps = let ctx = Univ.ContextSet.to_context ctx in let subst, ctx = Univ.abstract_universes true ctx in let args = instance_from_variable_context (List.rev sechyps) in - sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,subst,ctx) abs)::sl + sectab := (vars,f (Univ.UContext.instance ctx,args) exps, + g (sechyps,subst,ctx) abs)::sl let add_section_kn kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in @@ -453,10 +472,13 @@ let section_segment_of_mutual_inductive kn = let section_instance = function | VarRef id -> - if List.exists (fun (id',_,_,_) -> Names.id_eq id id') - (pi1 (List.hd !sectab)) - then Univ.Instance.empty, [||] - else raise Not_found + let eq = function + | Variable (id',_,_,_) -> Names.id_eq id id' + | Context _ -> false + in + if List.exists eq (pi1 (List.hd !sectab)) + then Univ.Instance.empty, [||] + else raise Not_found | ConstRef con -> Names.Cmap.find con (fst (pi2 (List.hd !sectab))) | IndRef (kn,_) | ConstructRef ((kn,_),_) -> -- cgit v1.2.3