diff options
Diffstat (limited to 'library/declare.ml')
-rw-r--r-- | library/declare.ml | 102 |
1 files changed, 76 insertions, 26 deletions
diff --git a/library/declare.ml b/library/declare.ml index 5f6f0fe4..c9992fff 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -9,7 +9,7 @@ (** This module is about the low-level declaration of logical objects *) open Pp -open Errors +open CErrors open Util open Names open Libnames @@ -149,7 +149,7 @@ let cache_constant ((sp,kn), obj) = obj.cst_was_seff <- false; if Global.exists_objlabel (Label.of_id (basename sp)) then constant_of_kn kn - else Errors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp)) + else CErrors.anomaly Pp.(str"Ex seff not found: " ++ Id.print(basename sp)) end else let () = check_exists sp in let kn', exported = Global.add_constant dir id obj.cst_decl in @@ -158,7 +158,7 @@ let cache_constant ((sp,kn), obj) = assert (eq_constant kn' (constant_of_kn kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); let cst = Global.lookup_constant kn' in - add_section_constant (cst.const_proj <> None) kn' cst.const_hyps; + add_section_constant cst.const_polymorphic kn' cst.const_hyps; Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; add_constant_kind (constant_of_kn kn) obj.cst_kind @@ -325,7 +325,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = let kn' = Global.add_mind dir id mie in assert (eq_mind kn' (mind_of_kn kn)); let mind = Global.lookup_mind kn' in - add_section_kn kn' mind.mind_hyps; + add_section_kn mind.mind_polymorphic kn' mind.mind_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names @@ -353,7 +353,8 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; mind_entry_polymorphic = false; mind_entry_universes = Univ.UContext.empty; - mind_entry_private = None }) + mind_entry_private = None; +}) type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry @@ -398,7 +399,7 @@ let declare_mind mie = let pr_rank i = pr_nth (i+1) let fixpoint_message indexes l = - Flags.if_verbose msg_info (match l with + Flags.if_verbose Feedback.msg_info (match l with | [] -> anomaly (Pp.str "no recursive definition") | [id] -> pr_id id ++ str " is recursively defined" ++ (match indexes with @@ -413,7 +414,7 @@ let fixpoint_message indexes l = | None -> mt ())) let cofixpoint_message l = - Flags.if_verbose msg_info (match l with + Flags.if_verbose Feedback.msg_info (match l with | [] -> anomaly (Pp.str "No corecursive definition.") | [id] -> pr_id id ++ str " is corecursively defined" | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++ @@ -423,15 +424,32 @@ let recursive_message isfix i l = (if isfix then fixpoint_message i else cofixpoint_message) l let definition_message id = - Flags.if_verbose msg_info (pr_id id ++ str " is defined") + Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined") let assumption_message id = - Flags.if_verbose msg_info (pr_id id ++ str " is assumed") + (* Changing "assumed" to "declared", "assuming" referring more to + the type of the object than to the name of the object (see + discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) + Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is declared") (** Global universe names, in a different summary *) -type universe_names = - (Univ.universe_level Idmap.t * Id.t Univ.LMap.t) +type universe_context_decl = polymorphic * Univ.universe_context_set + +let cache_universe_context (p, ctx) = + Global.push_context_set p ctx; + if p then Lib.add_section_context ctx + +let input_universe_context : universe_context_decl -> Libobject.obj = + declare_object + { (default_object "Global universe context state") with + cache_function = (fun (na, pi) -> cache_universe_context pi); + load_function = (fun _ (_, pi) -> cache_universe_context pi); + discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x); + classify_function = (fun a -> Keep a) } + +let declare_universe_context poly ctx = + Lib.add_anonymous_leaf (input_universe_context (poly, ctx)) (* Discharged or not *) type universe_decl = polymorphic * (Id.t * Univ.universe_level) list @@ -440,13 +458,13 @@ let cache_universes (p, l) = let glob = Universes.global_universe_names () in let glob', ctx = List.fold_left (fun ((idl,lid),ctx) (id, lev) -> - ((Idmap.add id lev idl, Univ.LMap.add lev id lid), - Univ.ContextSet.add_universe lev ctx)) + ((Idmap.add id (p, lev) idl, + Univ.LMap.add lev id lid), + Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l in - Global.push_context_set p ctx; - if p then Lib.add_section_context ctx; - Universes.set_global_universe_names glob' + cache_universe_context (p, ctx); + Universes.set_global_universe_names glob' let input_universes : universe_decl -> Libobject.obj = declare_object @@ -457,6 +475,12 @@ let input_universes : universe_decl -> Libobject.obj = classify_function = (fun a -> Keep a) } let do_universe poly l = + let in_section = Lib.sections_are_opened () in + let () = + if poly && not in_section then + user_err_loc (Loc.ghost, "Constraint", + str"Cannot declare polymorphic universes outside sections") + in let l = List.map (fun (l, id) -> let lev = Universes.new_univ_level (Global.current_dirpath ()) in @@ -467,8 +491,10 @@ let do_universe poly l = type constraint_decl = polymorphic * Univ.constraints let cache_constraints (na, (p, c)) = - Global.add_constraints c; - if p then Lib.add_section_context (Univ.ContextSet.add_constraints c Univ.ContextSet.empty) + let ctx = + Univ.ContextSet.add_constraints c + Univ.ContextSet.empty (* No declared universes here, just constraints *) + in cache_universe_context (p,ctx) let discharge_constraints (_, (p, c as a)) = if p then None else Some a @@ -483,16 +509,40 @@ let input_constraints : constraint_decl -> Libobject.obj = classify_function = (fun a -> Keep a) } let do_constraint poly l = - let u_of_id = - let names, _ = Universes.global_universe_names () in - fun (loc, id) -> - try Idmap.find id names - with Not_found -> - user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + let open Misctypes in + let u_of_id x = + match x with + | GProp -> Loc.dummy_loc, (false, Univ.Level.prop) + | GSet -> Loc.dummy_loc, (false, Univ.Level.set) + | GType None -> + user_err_loc (Loc.dummy_loc, "Constraint", + str "Cannot declare constraints on anonymous universes") + | GType (Some (loc, id)) -> + let id = Id.of_string id in + let names, _ = Universes.global_universe_names () in + try loc, Idmap.find id names + with Not_found -> + user_err_loc (loc, "Constraint", str "Undeclared universe " ++ pr_id id) + in + let in_section = Lib.sections_are_opened () in + let () = + if poly && not in_section then + user_err_loc (Loc.ghost, "Constraint", + str"Cannot declare polymorphic constraints outside sections") + in + let check_poly loc p loc' p' = + if poly then () + else if p || p' then + let loc = if p then loc else loc' in + user_err_loc (loc, "Constraint", + str "Cannot declare a global constraint on " ++ + str "a polymorphic universe, use " + ++ str "Polymorphic Constraint instead") in let constraints = List.fold_left (fun acc (l, d, r) -> - let lu = u_of_id l and ru = u_of_id r in - Univ.Constraint.add (lu, d, ru) acc) + let ploc, (p, lu) = u_of_id l and rloc, (p', ru) = u_of_id r in + check_poly ploc p rloc p'; + Univ.Constraint.add (lu, d, ru) acc) Univ.Constraint.empty l in Lib.add_anonymous_leaf (input_constraints (poly, constraints)) |