diff options
Diffstat (limited to 'interp/declare.ml')
| -rw-r--r-- | interp/declare.ml | 117 |
1 files changed, 60 insertions, 57 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index c55a6c69..a82e6b35 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -150,8 +150,8 @@ let register_side_effect (c, role) = ignore(add_leaf id o); update_tables c; match role with - | Safe_typing.Subproof -> () - | Safe_typing.Schema (ind, kind) -> !declare_scheme kind [|ind,c|] + | Subproof -> () + | Schema (ind, kind) -> !declare_scheme kind [|ind,c|] let declare_constant_common id cst = let o = inConstant cst in @@ -382,19 +382,44 @@ let inInductive : inductive_obj -> obj = discharge_function = discharge_inductive; rebuild_function = infer_inductive_subtyping } -let declare_projections mind = - let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in - match spec.mind_record with - | Some (Some (_, kns, pjs)) -> - Array.iteri (fun i kn -> - let id = Label.to_id (Constant.label kn) in - let entry = {proj_entry_ind = mind; proj_entry_arg = i} in - let kn' = declare_constant id (ProjectionEntry entry, - IsDefinition StructureComponent) - in - assert(Constant.equal kn kn')) kns; true,true - | Some None -> true,false - | None -> false,false +let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) = + let id = Label.to_id label in + let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in + Recordops.declare_primitive_projection p; + (* ^ needs to happen before declaring the constant, otherwise + Heads gets confused. *) + let univs = match univs with + | Monomorphic_ind_entry _ -> + (** Global constraints already defined through the inductive *) + Monomorphic_const_entry Univ.ContextSet.empty + | Polymorphic_ind_entry ctx -> + Polymorphic_const_entry ctx + | Cumulative_ind_entry ctx -> + Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx) + in + let term, types = match univs with + | Monomorphic_const_entry _ -> term, types + | Polymorphic_const_entry ctx -> + let u = Univ.UContext.instance ctx in + Vars.subst_instance_constr u term, Vars.subst_instance_constr u types + in + let entry = definition_entry ~types ~univs term in + ignore(declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent)) + +let declare_projections univs mind = + let env = Global.env () in + let mib = Environ.lookup_mind mind env in + match mib.mind_record with + | PrimRecord info -> + let iter_ind i (_, labs, _) = + let ind = (mind, i) in + let projs = Inductiveops.compute_projections env ind in + Array.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs + in + let () = Array.iteri iter_ind info in + true + | FakeRecord -> false + | NotRecord -> false (* for initial declaration *) let declare_mind mie = @@ -403,7 +428,7 @@ let declare_mind mie = | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in let mind = Global.mind_of_delta_kn kn in - let isrecord,isprim = declare_projections mind in + let isprim = declare_projections mie.mind_entry_universes mind in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; oname, isprim @@ -446,24 +471,20 @@ let assumption_message id = discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *) Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared") -(** Global universe names, in a different summary *) - -type universe_context_decl = polymorphic * Univ.ContextSet.t - -let cache_universe_context (p, ctx) = - Global.push_context_set p ctx; - if p then Lib.add_section_context ctx +(** Monomorphic universes need to survive sections. *) -let input_universe_context : universe_context_decl -> Libobject.obj = +let input_universe_context : Univ.ContextSet.t -> 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) } + { (default_object "Monomorphic section universes") with + cache_function = (fun (na, uctx) -> Global.push_context_set false uctx); + discharge_function = (fun (_, x) -> Some x); + classify_function = (fun a -> Dispose) } let declare_universe_context poly ctx = - Lib.add_anonymous_leaf (input_universe_context (poly, ctx)) + if poly then + (Global.push_context_set true ctx; Lib.add_section_context ctx) + else + Lib.add_anonymous_leaf (input_universe_context ctx) (** Global universes are not substitutive objects but global objects bound at the *library* or *module* level. The polymorphic flag is @@ -487,7 +508,7 @@ let add_universe src (dp, i) = Option.iter (fun poly -> let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in Global.push_context_set poly ctx; - Universes.add_global_universe level poly; + UnivNames.add_global_universe level poly; if poly then Lib.add_section_context ctx) optpoly @@ -538,7 +559,7 @@ let input_universe : universe_decl -> Libobject.obj = let declare_univ_binders gr pl = if Global.is_polymorphic gr then - Universes.register_universe_binders gr pl + UnivNames.register_universe_binders gr pl else let l = match gr with | ConstRef c -> Label.to_id @@ Constant.label c @@ -564,7 +585,7 @@ let do_universe poly l = in let l = List.map (fun {CAst.v=id} -> - let lev = Universes.new_univ_id () in + let lev = UnivGen.new_univ_id () in (id, lev)) l in let src = if poly then BoundUniv else UnqualifiedUniv in @@ -572,30 +593,11 @@ let do_universe poly l = ignore(Lib.add_leaf id (input_universe (src, lev)))) l -type constraint_decl = polymorphic * Univ.Constraint.t - -let cache_constraints (na, (p, c)) = - 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 - -let input_constraints : constraint_decl -> Libobject.obj = - let open Libobject in - declare_object - { (default_object "Global universe constraints") with - cache_function = cache_constraints; - load_function = (fun _ -> cache_constraints); - discharge_function = discharge_constraints; - classify_function = (fun a -> Keep a) } - let do_constraint poly l = + let open Univ in let u_of_id x = let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in - Universes.is_polymorphic level, level + UnivNames.is_polymorphic level, level in let in_section = Lib.sections_are_opened () in let () = @@ -614,7 +616,8 @@ let do_constraint poly l = let constraints = List.fold_left (fun acc (l, d, r) -> let p, lu = u_of_id l and p', ru = u_of_id r in check_poly p p'; - Univ.Constraint.add (lu, d, ru) acc) - Univ.Constraint.empty l + Constraint.add (lu, d, ru) acc) + Constraint.empty l in - Lib.add_anonymous_leaf (input_constraints (poly, constraints)) + let uctx = ContextSet.add_constraints constraints ContextSet.empty in + declare_universe_context poly uctx |