From 62fb849cf9410ddc2d9f355570f4fb859f3044c3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 25 Mar 2014 18:29:28 +0100 Subject: Adapt universe polymorphic branch to new handling of futures for delayed proofs. --- library/declare.ml | 6 +++--- library/declaremods.mli | 2 +- library/global.ml | 6 ++---- library/global.mli | 2 +- library/library.ml | 16 ++++++++-------- library/library.mli | 2 +- library/universes.ml | 8 ++++---- library/universes.mli | 2 +- 8 files changed, 21 insertions(+), 23 deletions(-) (limited to 'library') diff --git a/library/declare.ml b/library/declare.ml index 7fbf2f5ac..97445755f 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -64,7 +64,7 @@ let cache_variable ((sp,_),o) = | SectionLocalDef (de) -> let () = Global.push_named_def (id,de) in Explicit, de.const_entry_opaque, de.const_entry_polymorphic, - (Univ.ContextSet.of_context (Future.force de.const_entry_universes)) in + (Univ.ContextSet.of_context de.const_entry_universes) in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); add_section_variable id impl poly ctx; Dischargedhypsmap.set_discharged_hyps sp []; @@ -126,7 +126,7 @@ let open_constant i ((sp,kn), obj) = | (Def _ | Undef _) -> () | OpaqueDef lc -> match Opaqueproof.get_constraints lc with - | Some f when Future.is_val f -> Global.add_constraints (Future.force f) + | Some f when Future.is_val f -> Global.push_context (Future.force f) | _ -> () let exists_name id = @@ -201,7 +201,7 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types const_entry_type = types; const_entry_proj = None; const_entry_polymorphic = poly; - const_entry_universes = Future.from_val univs; + const_entry_universes = univs; const_entry_opaque = opaque; const_entry_feedback = None; const_entry_inline_code = inline} diff --git a/library/declaremods.mli b/library/declaremods.mli index 5ff471e69..a25247891 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -73,7 +73,7 @@ type library_objects val register_library : library_name -> Safe_typing.compiled_library -> library_objects -> Safe_typing.vodigest -> - Univ.constraints -> unit + Univ.universe_context -> unit val get_library_symbols_tbl : library_name -> Nativecode.symbol array diff --git a/library/global.ml b/library/global.ml index 812178bbb..74a2a1c0e 100644 --- a/library/global.ml +++ b/library/global.ml @@ -172,10 +172,8 @@ let type_of_global_in_context env r = | VarRef id -> Environ.named_type id env, Univ.UContext.empty | ConstRef c -> let cb = Environ.lookup_constant c env in - let univs = - if cb.const_polymorphic then Future.force cb.const_universes - else Univ.UContext.empty - in Typeops.type_of_constant_type env cb.Declarations.const_type, univs + let univs = Declareops.universes_of_polymorphic_constant cb in + Typeops.type_of_constant_type env cb.Declarations.const_type, univs | IndRef ind -> let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in let univs = diff --git a/library/global.mli b/library/global.mli index 410be961b..5995ff03f 100644 --- a/library/global.mli +++ b/library/global.mli @@ -94,7 +94,7 @@ val start_library : DirPath.t -> module_path val export : DirPath.t -> module_path * Safe_typing.compiled_library * Safe_typing.native_library val import : - Safe_typing.compiled_library -> Univ.constraints -> Safe_typing.vodigest -> + Safe_typing.compiled_library -> Univ.universe_context -> Safe_typing.vodigest -> module_path * Nativecode.symbol array (** {6 Misc } *) diff --git a/library/library.ml b/library/library.ml index 8521325b0..dc712ce02 100644 --- a/library/library.ml +++ b/library/library.ml @@ -39,7 +39,7 @@ type library_t = { library_deps : (compilation_unit_name * Safe_typing.vodigest) array; library_imports : compilation_unit_name array; library_digests : Safe_typing.vodigest; - library_extra_univs : Univ.constraints; + library_extra_univs : Univ.universe_context; } module LibraryOrdered = DirPath @@ -329,7 +329,7 @@ type 'a table_status = let opaque_tables = ref (LibraryMap.empty : (Term.constr table_status) LibraryMap.t) let univ_tables = - ref (LibraryMap.empty : (Univ.constraints table_status) LibraryMap.t) + ref (LibraryMap.empty : (Univ.universe_context table_status) LibraryMap.t) let add_opaque_table dp st = opaque_tables := LibraryMap.add dp st !opaque_tables @@ -354,7 +354,7 @@ let access_opaque_table dp i = add_opaque_table !opaque_tables dp i let access_univ_table dp i = access_table - (fetch_table "universe constraints of opaque proofs") + (fetch_table "universe contexts of opaque proofs") add_univ_table !univ_tables dp i (** Table of opaque terms from the library currently being compiled *) @@ -362,7 +362,7 @@ let access_univ_table dp i = module OpaqueTables = struct let a_constr = Future.from_val (Term.mkRel 1) - let a_univ = Future.from_val Univ.empty_constraint + let a_univ = Future.from_val Univ.UContext.empty let a_discharge : Opaqueproof.cooking_info list = [] let local_opaque_table = ref (Array.make 100 a_constr) @@ -440,7 +440,7 @@ let () = type seg_lib = library_disk type seg_univ = (* true = vivo, false = vi *) - Univ.constraints Future.computation array * Univ.constraints * bool + Univ.universe_context Future.computation array * Univ.universe_context * bool type seg_discharge = Opaqueproof.cooking_info list array type seg_proofs = Term.constr Future.computation array @@ -466,13 +466,13 @@ let intern_from_file f = add_opaque_table lmd.md_name (ToFetch (f,pos,digest)); let open Safe_typing in match univs with - | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.empty_constraint + | None -> mk_library lmd (Dvo_or_vi digest_lmd) Univ.UContext.empty | Some (utab,uall,true) -> add_univ_table lmd.md_name (Fetched utab); mk_library lmd (Dvivo (digest_lmd,digest_u)) uall | Some (utab,_,false) -> add_univ_table lmd.md_name (Fetched utab); - mk_library lmd (Dvo_or_vi digest_lmd) Univ.empty_constraint + mk_library lmd (Dvo_or_vi digest_lmd) Univ.UContext.empty let rec intern_library needed (dir, f) = (* Look if in the current logical environment *) @@ -731,7 +731,7 @@ let save_library_to ?todo dir f = | Some d -> assert(!Flags.compilation_mode = Flags.BuildVi); f ^ "i", (fun x -> Some (d x)), - (fun x -> Some (x,Univ.empty_constraint,false)), (fun x -> Some x) in + (fun x -> Some (x,Univ.UContext.empty,false)), (fun x -> Some x) in Opaqueproof.reset_indirect_creator (); let cenv, seg, ast = Declaremods.end_library dir in let opaque_table, univ_table, disch_table, f2t_map = diff --git a/library/library.mli b/library/library.mli index 16664d880..fc043aab6 100644 --- a/library/library.mli +++ b/library/library.mli @@ -31,7 +31,7 @@ val require_library_from_file : (** Segments of a library *) type seg_lib type seg_univ = (* cst, all_cst, finished? *) - Univ.constraints Future.computation array * Univ.constraints * bool + Univ.universe_context Future.computation array * Univ.universe_context * bool type seg_discharge = Opaqueproof.cooking_info list array type seg_proofs = Term.constr Future.computation array diff --git a/library/universes.ml b/library/universes.ml index 2b42e3fe8..138a248f0 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -63,7 +63,7 @@ let unsafe_instance_from ctx = let fresh_constant_instance env c = let cb = lookup_constant c env in if cb.Declarations.const_polymorphic then - let (inst,_), ctx = fresh_instance_from (Future.force cb.Declarations.const_universes) in + let (inst,_), ctx = fresh_instance_from (Declareops.universes_of_constant cb) in ((c, inst), ctx) else ((c,Instance.empty), ContextSet.empty) @@ -84,7 +84,7 @@ let fresh_constructor_instance env (ind,i) = let unsafe_constant_instance env c = let cb = lookup_constant c env in if cb.Declarations.const_polymorphic then - let inst, ctx = unsafe_instance_from (Future.force cb.Declarations.const_universes) in + let inst, ctx = unsafe_instance_from (Declareops.universes_of_constant cb) in ((c, inst), ctx) else ((c,Instance.empty), UContext.empty) @@ -183,7 +183,7 @@ let type_of_reference env r = let cb = Environ.lookup_constant c env in let ty = Typeops.type_of_constant_type env cb.const_type in if cb.const_polymorphic then - let (inst, subst), ctx = fresh_instance_from (Future.force cb.const_universes) in + let (inst, subst), ctx = fresh_instance_from (Declareops.universes_of_constant cb) in Vars.subst_univs_constr subst ty, ctx else ty, ContextSet.empty @@ -676,7 +676,7 @@ let restrict_universe_context (univs,csts) s = csts Constraint.empty in (univs', csts') -let simplify_universe_context (univs,csts) s = +let simplify_universe_context (univs,csts) = let uf = UF.create () in let noneqs = Constraint.fold (fun (l,d,r) noneqs -> diff --git a/library/universes.mli b/library/universes.mli index 150686d73..ab217e872 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -171,7 +171,7 @@ val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds val universes_of_constr : constr -> universe_set val shrink_universe_context : universe_context_set -> universe_set -> universe_context_set val restrict_universe_context : universe_context_set -> universe_set -> universe_context_set -val simplify_universe_context : universe_context_set -> universe_set -> +val simplify_universe_context : universe_context_set -> universe_context_set * universe_level_subst val refresh_constraints : universes -> universe_context_set -> universe_context_set * universes -- cgit v1.2.3