diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/assumptions.ml | 8 | ||||
| -rw-r--r-- | library/declare.ml | 83 | ||||
| -rw-r--r-- | library/declare.mli | 10 | ||||
| -rw-r--r-- | library/decls.ml | 11 | ||||
| -rw-r--r-- | library/decls.mli | 5 | ||||
| -rw-r--r-- | library/global.ml | 48 | ||||
| -rw-r--r-- | library/global.mli | 24 | ||||
| -rw-r--r-- | library/globnames.ml | 49 | ||||
| -rw-r--r-- | library/globnames.mli | 10 | ||||
| -rw-r--r-- | library/heads.ml | 23 | ||||
| -rw-r--r-- | library/impargs.ml | 51 | ||||
| -rw-r--r-- | library/impargs.mli | 2 | ||||
| -rw-r--r-- | library/kindops.ml | 2 | ||||
| -rw-r--r-- | library/lib.ml | 41 | ||||
| -rw-r--r-- | library/lib.mli | 16 | ||||
| -rw-r--r-- | library/library.mllib | 1 | ||||
| -rw-r--r-- | library/universes.ml | 647 | ||||
| -rw-r--r-- | library/universes.mli | 170 |
18 files changed, 1074 insertions, 127 deletions
diff --git a/library/assumptions.ml b/library/assumptions.ml index b1f133ac3..9cfe531ce 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -204,7 +204,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) = | Case (_,e1,e2,e_array) -> (iter e1)**(iter e2)**(iter_array e_array) | Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) -> (iter_array e1_array) ** (iter_array e2_array) - | Const kn -> do_memoize_kn kn + | Const (kn,_) -> do_memoize_kn kn | _ -> identity2 (* closed atomic types + rel *) and iter_array a = Array.fold_right (fun e f -> (iter e)**f) a identity2 in iter t s acc @@ -222,11 +222,7 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) = and add_kn kn s acc = let cb = lookup_constant kn in let do_type cst = - let ctype = - match cb.Declarations.const_type with - | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level) - | NonPolymorphicType t -> t - in + let ctype = cb.Declarations.const_type in (s,ContextObjectMap.add cst ctype acc) in let (s,acc) = diff --git a/library/declare.ml b/library/declare.ml index c0c4dd571..452504bf0 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -44,36 +44,40 @@ let if_xml f x = if !Flags.xml_export then f x else () type section_variable_entry = | SectionLocalDef of definition_entry - | SectionLocalAssum of types * bool (* Implicit status *) + | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind let cache_variable ((sp,_),o) = match o with - | Inl cst -> Global.add_constraints cst + | Inl ctx -> Global.push_context_set ctx | Inr (id,(p,d,mk)) -> (* Constr raisonne sur les noms courts *) if variable_exists id then alreadydeclared (pr_id id ++ str " already exists"); - let impl,opaq,cst = match d with (* Fails if not well-typed *) - | SectionLocalAssum (ty, impl) -> - let cst = Global.push_named_assum (id,ty) in - let impl = if impl then Implicit else Explicit in - impl, true, cst - | SectionLocalDef de -> - let cst = Global.push_named_def (id,de) in - Explicit, de.const_entry_opaque, cst in + + let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) + | SectionLocalAssum ((ty,ctx),poly,impl) -> + let () = Global.push_named_assum ((id,ty),ctx) in + let impl = if impl then Implicit else Explicit in + impl, true, poly, ctx + | SectionLocalDef (de) -> + let () = Global.push_named_def (id,de) in + Explicit, de.const_entry_opaque, de.const_entry_polymorphic, + (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; + add_section_variable id impl poly ctx; Dischargedhypsmap.set_discharged_hyps sp []; - add_variable_data id (p,opaq,cst,mk) + add_variable_data id (p,opaq,ctx,poly,mk) let discharge_variable (_,o) = match o with - | Inr (id,_) -> Some (Inl (variable_constraints id)) + | Inr (id,_) -> + if variable_polymorphic id then None + else Some (Inl (variable_context id)) | Inl _ -> Some o type variable_obj = - (Univ.constraints, Id.t * variable_declaration) union + (Univ.ContextSet.t, Id.t * variable_declaration) union let inVariable : variable_obj -> obj = declare_object { (default_object "VARIABLE") with @@ -139,7 +143,8 @@ let cache_constant ((sp,kn), obj) = let kn' = Global.add_constant dir id obj.cst_decl in assert (eq_constant kn' (constant_of_kn kn)); Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn)); - add_section_constant kn' (Global.lookup_constant kn').const_hyps; + let cst = Global.lookup_constant kn' in + add_section_constant (cst.const_proj <> None) kn' cst.const_hyps; Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps; add_constant_kind (constant_of_kn kn) obj.cst_kind @@ -150,16 +155,18 @@ let discharged_hyps kn sechyps = let discharge_constant ((sp, kn), obj) = let con = constant_of_kn kn in + let from = Global.lookup_constant con in let modlist = replacement_context () in - let hyps = section_segment_of_constant con in + let hyps,uctx = section_segment_of_constant con in let new_hyps = (discharged_hyps kn hyps) @ obj.cst_hyps in - let abstract = named_of_variable_context hyps in + let abstract = (named_of_variable_context hyps, uctx) in let new_decl = GlobalRecipe{ from; info = { Opaqueproof.modlist; abstract}} in Some { obj with cst_hyps = new_hyps; cst_decl = new_decl; } (* Hack to reduce the size of .vo: we keep only what load/open needs *) -let dummy_constant_entry = ConstantEntry (ParameterEntry (None,mkProp,None)) +let dummy_constant_entry = + ConstantEntry (ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None)) let dummy_constant cst = { cst_decl = dummy_constant_entry; @@ -187,6 +194,18 @@ let declare_constant_common id cst = Notation.declare_ref_arguments_scope (ConstRef c); c +let definition_entry ?(opaque=false) ?types + ?(poly=false) ?(univs=Univ.UContext.empty) body = + { const_entry_body = Future.from_val (body,Declareops.no_seff); + const_entry_secctx = None; + const_entry_type = types; + const_entry_proj = None; + const_entry_polymorphic = poly; + const_entry_universes = univs; + const_entry_opaque = opaque; + const_entry_feedback = None; + const_entry_inline_code = false} + let declare_scheme = ref (fun _ _ -> assert false) let set_declare_scheme f = declare_scheme := f let declare_sideff se = @@ -203,8 +222,7 @@ let declare_sideff se = in let ty_of cb = match cb.Declarations.const_type with - | Declarations.NonPolymorphicType t -> Some t - | _ -> None in + | (* Declarations.NonPolymorphicType *)t -> Some t in let cst_of cb = let pt, opaque = pt_opaque_of cb in let ty = ty_of cb in @@ -215,6 +233,9 @@ let declare_sideff se = const_entry_opaque = opaque; const_entry_inline_code = false; const_entry_feedback = None; + const_entry_polymorphic = cb.const_polymorphic; + const_entry_universes = Future.join cb.const_universes; + const_entry_proj = None; }); cst_hyps = [] ; cst_kind = Decl_kinds.IsDefinition Decl_kinds.Definition; @@ -252,16 +273,11 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) = let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in kn -let declare_definition ?(internal=UserVerbose) +let declare_definition ?(internal=UserVerbose) ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false) - id ?types body = + ?(poly=false) id ?types (body,ctx) = let cb = - { Entries.const_entry_body = body; - const_entry_type = types; - const_entry_opaque = opaque; - const_entry_inline_code = false; - const_entry_secctx = None; - const_entry_feedback = None } + definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body in declare_constant ~internal ~local id (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind) @@ -311,7 +327,8 @@ let cache_inductive ((sp,kn),(dhyps,mie)) = let _,dir,_ = repr_kn kn in let kn' = Global.add_mind dir id mie in assert (eq_mind kn' (mind_of_kn kn)); - add_section_kn kn' (Global.lookup_mind kn').mind_hyps; + let mind = Global.lookup_mind kn' in + add_section_kn kn' mind.mind_hyps; Dischargedhypsmap.set_discharged_hyps sp dhyps; List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names @@ -319,9 +336,9 @@ let discharge_inductive ((sp,kn),(dhyps,mie)) = let mind = Global.mind_of_delta_kn kn in let mie = Global.lookup_mind mind in let repl = replacement_context () in - let sechyps = section_segment_of_mutual_inductive mind in + let sechyps,uctx = section_segment_of_mutual_inductive mind in Some (discharged_hyps kn sechyps, - Discharge.process_inductive (named_of_variable_context sechyps) repl mie) + Discharge.process_inductive (named_of_variable_context sechyps,uctx) repl mie) let dummy_one_inductive_entry mie = { mind_entry_typename = mie.mind_entry_typename; @@ -335,7 +352,9 @@ let dummy_inductive_entry (_,m) = ([],{ mind_entry_params = []; mind_entry_record = false; mind_entry_finite = true; - mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds }) + mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds; + mind_entry_polymorphic = false; + mind_entry_universes = Univ.UContext.empty }) type inductive_obj = Dischargedhypsmap.discharged_hyps * mutual_inductive_entry diff --git a/library/declare.mli b/library/declare.mli index 663d240dc..848bab618 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -23,7 +23,7 @@ open Decl_kinds type section_variable_entry = | SectionLocalDef of definition_entry - | SectionLocalAssum of types * bool (** Implicit status *) + | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *) type variable_declaration = DirPath.t * section_variable_entry * logical_kind @@ -47,12 +47,18 @@ type internal_flag = | KernelSilent | UserVerbose +(* Defaut definition entries, transparent with no secctx or proj information *) +val definition_entry : ?opaque:bool -> ?types:types -> + ?poly:polymorphic -> ?univs:Univ.universe_context -> + constr -> definition_entry + val declare_constant : ?internal:internal_flag -> ?local:bool -> Id.t -> constant_declaration -> constant val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> - ?local:bool -> Id.t -> ?types:constr -> Entries.const_entry_body -> constant + ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> + constr Univ.in_universe_context_set -> constant (** Since transparent constant's side effects are globally declared, we * need that *) diff --git a/library/decls.ml b/library/decls.ml index 2d8807f80..811d09667 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -18,17 +18,18 @@ open Libnames (** Datas associated to section variables and local definitions *) type variable_data = - DirPath.t * bool (* opacity *) * Univ.constraints * logical_kind + DirPath.t * bool (* opacity *) * Univ.universe_context_set * polymorphic * logical_kind let vartab = Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE" let add_variable_data id o = vartab := Id.Map.add id o !vartab -let variable_path id = let (p,_,_,_) = Id.Map.find id !vartab in p -let variable_opacity id = let (_,opaq,_,_) = Id.Map.find id !vartab in opaq -let variable_kind id = let (_,_,_,k) = Id.Map.find id !vartab in k -let variable_constraints id = let (_,_,cst,_) = Id.Map.find id !vartab in cst +let variable_path id = let (p,_,_,_,_) = Id.Map.find id !vartab in p +let variable_opacity id = let (_,opaq,_,_,_) = Id.Map.find id !vartab in opaq +let variable_kind id = let (_,_,_,_,k) = Id.Map.find id !vartab in k +let variable_context id = let (_,_,ctx,_,_) = Id.Map.find id !vartab in ctx +let variable_polymorphic id = let (_,_,_,p,_) = Id.Map.find id !vartab in p let variable_secpath id = let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in diff --git a/library/decls.mli b/library/decls.mli index f45e4f121..6e9d4a4ab 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -17,14 +17,15 @@ open Decl_kinds (** Registration and access to the table of variable *) type variable_data = - DirPath.t * bool (** opacity *) * Univ.constraints * logical_kind + DirPath.t * bool (** opacity *) * Univ.universe_context_set * polymorphic * logical_kind val add_variable_data : variable -> variable_data -> unit val variable_path : variable -> DirPath.t val variable_secpath : variable -> qualid val variable_kind : variable -> logical_kind val variable_opacity : variable -> bool -val variable_constraints : variable -> Univ.constraints +val variable_context : variable -> Univ.universe_context_set +val variable_polymorphic : variable -> polymorphic val variable_exists : variable -> bool (** Registration and access to the table of constants *) diff --git a/library/global.ml b/library/global.ml index a8121d15f..c56bc9e77 100644 --- a/library/global.ml +++ b/library/global.ml @@ -70,9 +70,12 @@ let globalize_with_summary fs f = let i2l = Label.of_id -let push_named_assum a = globalize (Safe_typing.push_named_assum a) -let push_named_def d = globalize (Safe_typing.push_named_def d) +let push_named_assum a = globalize0 (Safe_typing.push_named_assum a) +let push_named_def d = globalize0 (Safe_typing.push_named_def d) let add_constraints c = globalize0 (Safe_typing.add_constraints c) +let push_context_set c = globalize0 (Safe_typing.push_context_set c) +let push_context c = globalize0 (Safe_typing.push_context c) + let set_engagement c = globalize0 (Safe_typing.set_engagement c) let add_constant dir id d = globalize (Safe_typing.add_constant dir (i2l id) d) let add_mind dir id mie = globalize (Safe_typing.add_mind dir (i2l id) mie) @@ -101,6 +104,7 @@ let named_context_val () = named_context_val (env()) let lookup_named id = lookup_named id (env()) let lookup_constant kn = lookup_constant kn (env()) let lookup_inductive ind = Inductive.lookup_mind_specif (env()) ind +let lookup_pinductive (ind,_) = Inductive.lookup_mind_specif (env()) ind let lookup_mind kn = lookup_mind kn (env()) let lookup_module mp = lookup_module mp (env()) @@ -139,19 +143,43 @@ let env_of_context hyps = open Globnames -let type_of_reference env = function +(** Build a fresh instance for a given context, its associated substitution and + the instantiated constraints. *) + +let type_of_global_unsafe r = + let env = env() in + match r with | VarRef id -> Environ.named_type id env - | ConstRef c -> Typeops.type_of_constant env c + | ConstRef c -> + let cb = Environ.lookup_constant c env in cb.Declarations.const_type + | IndRef ind -> + let (mib, oib) = Inductive.lookup_mind_specif env ind in + oib.Declarations.mind_arity.Declarations.mind_user_arity + | ConstructRef cstr -> + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + let inst = Univ.UContext.instance mib.Declarations.mind_universes in + Inductive.type_of_constructor (cstr,inst) specif + + +let is_polymorphic r = + let env = env() in + match r with + | VarRef id -> false + | ConstRef c -> + let cb = Environ.lookup_constant c env in cb.Declarations.const_polymorphic | IndRef ind -> - let specif = Inductive.lookup_mind_specif env ind in - Inductive.type_of_inductive env specif + let (mib, oib) = Inductive.lookup_mind_specif env ind in + mib.Declarations.mind_polymorphic | ConstructRef cstr -> - let specif = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Inductive.type_of_constructor cstr specif + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + mib.Declarations.mind_polymorphic -let type_of_global t = type_of_reference (env ()) t +let current_dirpath () = + Safe_typing.current_dirpath (safe_env ()) +let with_global f = + let (a, ctx) = f (env ()) (current_dirpath ()) in + push_context_set ctx; a (* spiwack: register/unregister functions for retroknowledge *) let register field value by_clause = diff --git a/library/global.mli b/library/global.mli index e11e1c017..b6825ffa5 100644 --- a/library/global.mli +++ b/library/global.mli @@ -33,13 +33,19 @@ val add_constraints : Univ.constraints -> unit (** Variables, Local definitions, constants, inductive types *) -val push_named_assum : (Id.t * Term.types) -> Univ.constraints -val push_named_def : (Id.t * Entries.definition_entry) -> Univ.constraints +val push_named_assum : (Id.t * Constr.types) Univ.in_universe_context_set -> unit +val push_named_def : (Id.t * Entries.definition_entry) -> unit + val add_constant : DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant val add_mind : DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive +val add_constraints : Univ.constraints -> unit + +val push_context : Univ.universe_context -> unit +val push_context_set : Univ.universe_context_set -> unit + (** Non-interactive modules and module types *) val add_module : @@ -72,6 +78,8 @@ val lookup_named : variable -> Context.named_declaration val lookup_constant : constant -> Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body +val lookup_pinductive : Constr.pinductive -> + Declarations.mutual_inductive_body * Declarations.one_inductive_body val lookup_mind : mutual_inductive -> Declarations.mutual_inductive_body val lookup_module : module_path -> Declarations.module_body val lookup_modtype : module_path -> Declarations.module_type_body @@ -94,11 +102,14 @@ val import : (** Function to get an environment from the constants part of the global * environment and a given context. *) -val type_of_global : Globnames.global_reference -> Term.types val env_of_context : Environ.named_context_val -> Environ.env val join_safe_environment : unit -> unit +val is_polymorphic : Globnames.global_reference -> bool + +(* val type_of_global : Globnames.global_reference -> types Univ.in_universe_context_set *) +val type_of_global_unsafe : Globnames.global_reference -> Constr.types (** {6 Retroknowledge } *) @@ -109,5 +120,10 @@ val register_inline : constant -> unit (** {6 Oracle } *) -val set_strategy : 'a Names.tableKey -> Conv_oracle.level -> unit +val set_strategy : Names.constant Names.tableKey -> Conv_oracle.level -> unit + +(* Modifies the global state, registering new universes *) + +val current_dirpath : unit -> Names.dir_path +val with_global : (Environ.env -> Names.dir_path -> 'a Univ.in_universe_context_set) -> 'a diff --git a/library/globnames.ml b/library/globnames.ml index 8a9e99621..c881e797e 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -38,19 +38,31 @@ let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef" let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef" -let subst_constructor subst ((kn,i),j as ref) = - let kn' = subst_ind subst kn in - if kn==kn' then ref, mkConstruct ref - else ((kn',i),j), mkConstruct ((kn',i),j) +let subst_constructor subst (ind,j as ref) = + let ind' = subst_ind subst ind in + if ind==ind' then ref, mkConstruct ref + else (ind',j), mkConstruct (ind',j) + +let subst_global_reference subst ref = match ref with + | VarRef var -> ref + | ConstRef kn -> + let kn' = subst_constant subst kn in + if kn==kn' then ref else ConstRef kn' + | IndRef ind -> + let ind' = subst_ind subst ind in + if ind==ind' then ref else IndRef ind' + | ConstructRef ((kn,i),j as c) -> + let c',t = subst_constructor subst c in + if c'==c then ref else ConstructRef c' let subst_global subst ref = match ref with | VarRef var -> ref, mkVar var | ConstRef kn -> - let kn',t = subst_con subst kn in + let kn',t = subst_con_kn subst kn in if kn==kn' then ref, mkConst kn else ConstRef kn', t - | IndRef (kn,i) -> - let kn' = subst_ind subst kn in - if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i) + | IndRef ind -> + let ind' = subst_ind subst ind in + if ind==ind' then ref, mkInd ind else IndRef ind', mkInd ind' | ConstructRef ((kn,i),j as c) -> let c',t = subst_constructor subst c in if c'==c then ref,t else ConstructRef c', t @@ -62,19 +74,26 @@ let canonical_gr = function | VarRef id -> VarRef id let global_of_constr c = match kind_of_term c with - | Const sp -> ConstRef sp - | Ind ind_sp -> IndRef ind_sp - | Construct cstr_cp -> ConstructRef cstr_cp + | Const (sp,u) -> ConstRef sp + | Ind (ind_sp,u) -> IndRef ind_sp + | Construct (cstr_cp,u) -> ConstructRef cstr_cp | Var id -> VarRef id | _ -> raise Not_found -let constr_of_global = function +let is_global c t = + match c, kind_of_term t with + | ConstRef c, Const (c', _) -> eq_constant c c' + | IndRef i, Ind (i', _) -> eq_ind i i' + | ConstructRef i, Construct (i', _) -> eq_constructor i i' + | VarRef id, Var id' -> id_eq id id' + | _ -> false + +let printable_constr_of_global = function | VarRef id -> mkVar id | ConstRef sp -> mkConst sp | ConstructRef sp -> mkConstruct sp | IndRef sp -> mkInd sp -let constr_of_reference = constr_of_global let reference_of_constr = global_of_constr let global_eq_gen eq_cst eq_ind eq_cons x y = @@ -179,10 +198,6 @@ type global_reference_or_constr = | IsGlobal of global_reference | IsConstr of constr -let constr_of_global_or_constr = function - | IsConstr c -> c - | IsGlobal gr -> constr_of_global gr - (** {6 Temporary function to brutally form kernel names from section paths } *) let encode_mind dir id = MutInd.make2 (MPfile dir) (Label.of_id id) diff --git a/library/globnames.mli b/library/globnames.mli index 5d717965e..5ea0c9de0 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -31,19 +31,21 @@ val destConstRef : global_reference -> constant val destIndRef : global_reference -> inductive val destConstructRef : global_reference -> constructor +val is_global : global_reference -> constr -> bool val subst_constructor : substitution -> constructor -> constructor * constr val subst_global : substitution -> global_reference -> global_reference * constr +val subst_global_reference : substitution -> global_reference -> global_reference -(** Turn a global reference into a construction *) -val constr_of_global : global_reference -> constr +(** This constr is not safe to be typechecked, universe polymorphism is not + handled here: just use for printing *) +val printable_constr_of_global : global_reference -> constr (** Turn a construction denoting a global reference into a global reference; raise [Not_found] if not a global reference *) val global_of_constr : constr -> global_reference (** Obsolete synonyms for constr_of_global and global_of_constr *) -val constr_of_reference : global_reference -> constr val reference_of_constr : constr -> global_reference module RefOrdered : sig @@ -87,8 +89,6 @@ type global_reference_or_constr = | IsGlobal of global_reference | IsConstr of constr -val constr_of_global_or_constr : global_reference_or_constr -> constr - (** {6 Temporary function to brutally form kernel names from section paths } *) val encode_mind : DirPath.t -> Id.t -> mutual_inductive diff --git a/library/heads.ml b/library/heads.ml index f64cdb05a..0faad827e 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -58,7 +58,7 @@ let variable_head id = Evalrefmap.find (EvalVarRef id) !head_map let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map let kind_of_head env t = - let rec aux k l t b = match kind_of_term (Reduction.whd_betaiotazeta t) with + let rec aux k l t b = match kind_of_term (Reduction.whd_betaiotazeta env t) with | Rel n when n > k -> NotImmediatelyComputableHead | Rel n -> FlexibleHead (k,k+1-n,List.length l,b) | Var id -> @@ -68,7 +68,7 @@ let kind_of_head env t = match pi2 (lookup_named id env) with | Some c -> aux k l c b | None -> NotImmediatelyComputableHead) - | Const cst -> + | Const (cst,_) -> (try on_subterm k l b (constant_head cst) with Not_found -> assert false) | Construct _ | CoFix _ -> @@ -85,6 +85,10 @@ let kind_of_head env t = | LetIn _ -> assert false | Meta _ | Evar _ -> NotImmediatelyComputableHead | App (c,al) -> aux k (Array.to_list al @ l) c b + | Proj (p,c) -> + (try on_subterm k (c :: l) b (constant_head p) + with Not_found -> assert false) + | Case (_,_,c,_) -> aux k [] c true | Fix ((i,j),_) -> let n = i.(j) in @@ -113,11 +117,18 @@ let kind_of_head env t = | x -> x in aux 0 [] t false +(* FIXME: maybe change interface here *) let compute_head = function | EvalConstRef cst -> - (match constant_opt_value (Global.env()) cst with + let env = Global.env() in + let cb = Environ.lookup_constant cst env in + let body = + if cb.Declarations.const_proj = None + then Declareops.body_of_constant cb else None + in + (match body with | None -> RigidHead (RigidParameter cst) - | Some c -> kind_of_head (Global.env()) c) + | Some c -> kind_of_head env c) | EvalVarRef id -> (match pi2 (Global.lookup_named id) with | Some c when not (Decls.variable_opacity id) -> @@ -140,8 +151,8 @@ let cache_head o = let subst_head_approximation subst = function | RigidHead (RigidParameter cst) as k -> - let cst,c = subst_con subst cst in - if isConst c && eq_constant (destConst c) cst then + let cst,c = subst_con_kn subst cst in + if isConst c && eq_constant (fst (destConst c)) cst then (* A change of the prefix of the constant *) k else diff --git a/library/impargs.ml b/library/impargs.ml index 1bcff8695..5a44b5bdb 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -169,7 +169,7 @@ let is_flexible_reference env bound depth f = | Rel n when n >= bound+depth -> (* inductive type *) false | Rel n when n >= depth -> (* previous argument *) true | Rel n -> (* since local definitions have been expanded *) false - | Const kn -> + | Const (kn,_) -> let cb = Environ.lookup_constant kn env in (match cb.const_body with Def _ -> true | _ -> false) | Var id -> @@ -214,6 +214,7 @@ let rec is_rigid_head t = match kind_of_term t with | Rel _ | Evar _ -> false | Ind _ | Const _ | Var _ | Sort _ -> true | Case (_,_,f,_) -> is_rigid_head f + | Proj (p,c) -> true | App (f,args) -> (match kind_of_term f with | Fix ((fi,i),_) -> is_rigid_head (args.(fi.(i))) @@ -401,7 +402,14 @@ let compute_semi_auto_implicits env f manual t = let compute_constant_implicits flags manual cst = let env = Global.env () in - compute_semi_auto_implicits env flags manual (Typeops.type_of_constant env cst) + let cb = Environ.lookup_constant cst env in + let ty = cb.const_type in + let impls = compute_semi_auto_implicits env flags manual ty in + impls + (* match cb.const_proj with *) + (* | None -> impls *) + (* | Some {proj_npars = n} -> *) + (* List.map (fun (x,args) -> x, CList.skipn_at_least n args) impls *) (*s Inductives and constructors. Their implicit arguments are stored in an array, indexed by the inductive number, of pairs $(i,v)$ where @@ -413,14 +421,15 @@ let compute_mib_implicits flags manual kn = let mib = lookup_mind kn env in let ar = Array.to_list - (Array.map (* No need to lift, arities contain no de Bruijn *) - (fun mip -> - (Name mip.mind_typename, None, type_of_inductive env (mib,mip))) + (Array.mapi (* No need to lift, arities contain no de Bruijn *) + (fun i mip -> + (** No need to care about constraints here *) + (Name mip.mind_typename, None, Global.type_of_global_unsafe (IndRef (kn,i)))) mib.mind_packets) in let env_ar = push_rel_context ar env in let imps_one_inductive i mip = let ind = (kn,i) in - let ar = type_of_inductive env (mib,mip) in + let ar = Global.type_of_global_unsafe (IndRef ind) in ((IndRef ind,compute_semi_auto_implicits env flags manual ar), Array.mapi (fun j c -> (ConstructRef (ind,j+1),compute_semi_auto_implicits env_ar flags manual c)) @@ -517,7 +526,7 @@ let section_segment_of_reference = function | ConstRef con -> section_segment_of_constant con | IndRef (kn,_) | ConstructRef ((kn,_),_) -> section_segment_of_mutual_inductive kn - | _ -> [] + | _ -> [], Univ.UContext.empty let adjust_side_condition p = function | LessArgsThan n -> LessArgsThan (n+p) @@ -532,24 +541,36 @@ let discharge_implicits (_,(req,l)) = | ImplLocal -> None | ImplInteractive (ref,flags,exp) -> (try - let vars = section_segment_of_reference ref in + let vars,_ = section_segment_of_reference ref in + (* let isproj = *) + (* match ref with *) + (* | ConstRef cst -> is_projection cst (Global.env ()) *) + (* | _ -> false *) + (* in *) let ref' = if isVarRef ref then ref else pop_global_reference ref in let extra_impls = impls_of_context vars in - let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in + let l' = + (* if isproj then [ref',snd (List.hd l)] *) + (* else *) + [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in Some (ImplInteractive (ref',flags,exp),l') with Not_found -> (* ref not defined in this section *) Some (req,l)) | ImplConstant (con,flags) -> (try let con' = pop_con con in - let vars = section_segment_of_constant con in + let vars,_ = section_segment_of_constant con in let extra_impls = impls_of_context vars in - let l' = [ConstRef con',List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in + let newimpls = + (* if is_projection con (Global.env()) then (snd (List.hd l)) *) + (* else *) List.map (add_section_impls vars extra_impls) (snd (List.hd l)) + in + let l' = [ConstRef con',newimpls] in Some (ImplConstant (con',flags),l') with Not_found -> (* con not defined in this section *) Some (req,l)) | ImplMutualInductive (kn,flags) -> (try let l' = List.map (fun (gr, l) -> - let vars = section_segment_of_reference gr in + let vars,_ = section_segment_of_reference gr in let extra_impls = impls_of_context vars in ((if isVarRef gr then gr else pop_global_reference gr), List.map (add_section_impls vars extra_impls) l)) l @@ -659,10 +680,14 @@ let check_rigidity isrigid = if not isrigid then errorlabstrm "" (strbrk "Multiple sequences of implicit arguments available only for references that cannot be applied to an arbitrarily large number of arguments.") +let projection_implicits env p (x, impls) = + let pb = Environ.lookup_projection p env in + x, CList.skipn_at_least pb.Declarations.proj_npars impls + let declare_manual_implicits local ref ?enriching l = let flags = !implicit_args in let env = Global.env () in - let t = Global.type_of_global ref in + let t = Global.type_of_global_unsafe ref in let enriching = Option.default flags.auto enriching in let isrigid,autoimpls = compute_auto_implicits env flags enriching t in let l' = match l with diff --git a/library/impargs.mli b/library/impargs.mli index e70cff838..8ad86bdff 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -129,6 +129,8 @@ val make_implicits_list : implicit_status list -> implicits_list list val drop_first_implicits : int -> implicits_list -> implicits_list +val projection_implicits : env -> projection -> implicits_list -> implicits_list + val select_impargs_size : int -> implicits_list list -> implicit_status list val select_stronger_impargs : implicits_list list -> implicit_status list diff --git a/library/kindops.ml b/library/kindops.ml index 6e6c7527b..b8337f5d7 100644 --- a/library/kindops.ml +++ b/library/kindops.ml @@ -24,7 +24,7 @@ let string_of_theorem_kind = function | Corollary -> "Corollary" let string_of_definition_kind def = - let (locality, kind) = def in + let (locality, poly, kind) = def in let error () = Errors.anomaly (Pp.str "Internal definition kind") in match kind with | Definition -> diff --git a/library/lib.ml b/library/lib.ml index 331196565..31f983595 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -380,11 +380,14 @@ let find_opening_node id = *) type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types + type variable_context = variable_info list -type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap.t +type abstr_list = variable_context Univ.in_universe_context Names.Cmap.t * + variable_context Univ.in_universe_context Names.Mindmap.t let sectab = - Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list * + Summary.ref ([] : ((Names.Id.t * Decl_kinds.binding_kind * + Decl_kinds.polymorphic * Univ.universe_context_set) list * Opaqueproof.work_list * abstr_list) list) ~name:"section-context" @@ -392,18 +395,19 @@ let add_section () = sectab := ([],(Names.Cmap.empty,Names.Mindmap.empty), (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab -let add_section_variable id impl = +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)::vars,repl,abs)::sl + sectab := ((id,impl,poly,ctx)::vars,repl,abs)::sl let extract_hyps (secs,ohyps) = let rec aux = function - | ((id,impl)::idl,(id',b,t)::hyps) when Names.Id.equal id id' -> - (id',impl,b,t) :: aux (idl,hyps) + | ((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 | (id::idl,hyps) -> aux (idl,hyps) - | [], _ -> [] + | [], _ -> [],Univ.ContextSet.empty in aux (secs,ohyps) let instance_from_variable_context sign = @@ -413,23 +417,26 @@ let instance_from_variable_context sign = | [] -> [] in Array.of_list (inst_rec sign) -let named_of_variable_context = List.map (fun (id,_,b,t) -> (id,b,t)) - +let named_of_variable_context ctx = List.map (fun (id,_,b,t) -> (id,b,t)) ctx + let add_section_replacement f g hyps = match !sectab with | [] -> () | (vars,exps,abs)::sl -> - let sechyps = extract_hyps (vars,hyps) in + let sechyps,ctx = extract_hyps (vars,hyps) in + let ctx = Univ.ContextSet.to_context ctx in let args = instance_from_variable_context (List.rev sechyps) in - sectab := (vars,f args exps,g sechyps abs)::sl + sectab := (vars,f (Univ.UContext.instance ctx,args) exps,g (sechyps,ctx) abs)::sl let add_section_kn kn = let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in add_section_replacement f f -let add_section_constant kn = +let add_section_constant is_projection kn = + (* let g x (l1,l2) = (Names.Cmap.add kn (Univ.Instance.empty,[||]) l1,l2) in *) let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in - add_section_replacement f f + (* if is_projection then add_section_replacement g f *) + (* else *) add_section_replacement f f let replacement_context () = pi2 (List.hd !sectab) @@ -445,7 +452,9 @@ let rec list_mem_assoc x = function let section_instance = function | VarRef id -> - if list_mem_assoc id (pi1 (List.hd !sectab)) then [||] + if List.exists (fun (id',_,_,_) -> Names.id_eq id id') + (pi1 (List.hd !sectab)) + then Univ.Instance.empty, [||] else raise Not_found | ConstRef con -> Names.Cmap.find con (fst (pi2 (List.hd !sectab))) @@ -459,8 +468,8 @@ let full_replacement_context () = List.map pi2 !sectab let full_section_segment_of_constant con = List.map (fun (vars,_,(x,_)) -> fun hyps -> named_of_variable_context - (try Names.Cmap.find con x - with Not_found -> extract_hyps (vars, hyps))) !sectab + (try fst (Names.Cmap.find con x) + with Not_found -> fst (extract_hyps (vars, hyps)))) !sectab (*************) (* Sections. *) diff --git a/library/lib.mli b/library/lib.mli index 8975acd9a..759a1a135 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -161,23 +161,23 @@ val xml_close_section : (Names.Id.t -> unit) Hook.t (** {6 Section management for discharge } *) type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types -type variable_context = variable_info list +type variable_context = variable_info list val instance_from_variable_context : variable_context -> Names.Id.t array val named_of_variable_context : variable_context -> Context.named_context -val section_segment_of_constant : Names.constant -> variable_context -val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context +val section_segment_of_constant : Names.constant -> variable_context Univ.in_universe_context +val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context Univ.in_universe_context -val section_instance : Globnames.global_reference -> Names.Id.t array +val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array val is_in_section : Globnames.global_reference -> bool -val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> unit +val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit -val add_section_constant : Names.constant -> Context.named_context -> unit +val add_section_constant : bool (* is_projection *) -> + Names.constant -> Context.named_context -> unit val add_section_kn : Names.mutual_inductive -> Context.named_context -> unit -val replacement_context : unit -> - (Names.Id.t array Names.Cmap.t * Names.Id.t array Names.Mindmap.t) +val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) diff --git a/library/library.mllib b/library/library.mllib index 2568bcc18..6a58a1057 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -5,6 +5,7 @@ Libobject Summary Nametab Global +Universes Lib Declaremods Loadpath diff --git a/library/universes.ml b/library/universes.ml new file mode 100644 index 000000000..79286792d --- /dev/null +++ b/library/universes.ml @@ -0,0 +1,647 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Pp +open Names +open Term +open Context +open Environ +open Locus +open Univ + +(* Generator of levels *) +let new_univ_level, set_remote_new_univ_level = + RemoteCounter.new_counter ~name:"Universes" 0 ~incr:((+) 1) + ~build:(fun n -> Univ.Level.make (Global.current_dirpath ()) n) + +let new_univ_level _ = new_univ_level () + (* Univ.Level.make db (new_univ_level ()) *) + +let fresh_level () = new_univ_level (Global.current_dirpath ()) + +(* TODO: remove *) +let new_univ dp = Univ.Universe.make (new_univ_level dp) +let new_Type dp = mkType (new_univ dp) +let new_Type_sort dp = Type (new_univ dp) + +let fresh_universe_instance ctx = + Instance.subst_fn (fun _ -> new_univ_level (Global.current_dirpath ())) + (UContext.instance ctx) + +let fresh_instance_from_context ctx = + let inst = fresh_universe_instance ctx in + let subst = make_universe_subst inst ctx in + let constraints = instantiate_univ_context subst ctx in + (inst, subst), constraints + +let fresh_instance ctx = + let s = ref LSet.empty in + let inst = + Instance.subst_fn (fun _ -> + let u = new_univ_level (Global.current_dirpath ()) in + s := LSet.add u !s; u) + (UContext.instance ctx) + in !s, inst + +let fresh_instance_from ctx = + let ctx', inst = fresh_instance ctx in + let subst = make_universe_subst inst ctx in + let constraints = instantiate_univ_context subst ctx in + (inst, subst), (ctx', constraints) + +(** Fresh universe polymorphic construction *) + +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.join cb.Declarations.const_universes) in + ((c, inst), ctx) + else ((c,Instance.empty), ContextSet.empty) + +let fresh_inductive_instance env ind = + let mib, mip = Inductive.lookup_mind_specif env ind in + if mib.Declarations.mind_polymorphic then + let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes in + ((ind,inst), ctx) + else ((ind,Instance.empty), ContextSet.empty) + +let fresh_constructor_instance env (ind,i) = + let mib, mip = Inductive.lookup_mind_specif env ind in + if mib.Declarations.mind_polymorphic then + let (inst,_), ctx = fresh_instance_from mib.Declarations.mind_universes in + (((ind,i),inst), ctx) + else (((ind,i),Instance.empty), ContextSet.empty) + +open Globnames +let fresh_global_instance env gr = + match gr with + | VarRef id -> mkVar id, ContextSet.empty + | ConstRef sp -> + let c, ctx = fresh_constant_instance env sp in + mkConstU c, ctx + | ConstructRef sp -> + let c, ctx = fresh_constructor_instance env sp in + mkConstructU c, ctx + | IndRef sp -> + let c, ctx = fresh_inductive_instance env sp in + mkIndU c, ctx + +let constr_of_global gr = + let c, ctx = fresh_global_instance (Global.env ()) gr in + Global.push_context_set ctx; c + +let constr_of_global_univ (gr,u) = + match gr with + | VarRef id -> mkVar id + | ConstRef sp -> mkConstU (sp,u) + | ConstructRef sp -> mkConstructU (sp,u) + | IndRef sp -> mkIndU (sp,u) + +let fresh_global_or_constr_instance env = function + | IsConstr c -> c, ContextSet.empty + | IsGlobal gr -> fresh_global_instance env gr + +let global_of_constr c = + match kind_of_term c with + | Const (c, u) -> ConstRef c, u + | Ind (i, u) -> IndRef i, u + | Construct (c, u) -> ConstructRef c, u + | Var id -> VarRef id, Instance.empty + | _ -> raise Not_found + +let global_app_of_constr c = + match kind_of_term c with + | Const (c, u) -> (ConstRef c, u), None + | Ind (i, u) -> (IndRef i, u), None + | Construct (c, u) -> (ConstructRef c, u), None + | Var id -> (VarRef id, Instance.empty), None + | Proj (p, c) -> (ConstRef p, Instance.empty), Some c + | _ -> raise Not_found + +open Declarations + +let type_of_reference env r = + match r with + | VarRef id -> Environ.named_type id env, ContextSet.empty + | ConstRef c -> + let cb = Environ.lookup_constant c env in + if cb.const_polymorphic then + let (inst, subst), ctx = fresh_instance_from (Future.join cb.const_universes) in + Vars.subst_univs_constr subst cb.const_type, ctx + else cb.const_type, ContextSet.empty + + | IndRef ind -> + let (mib, oib) = Inductive.lookup_mind_specif env ind in + if mib.mind_polymorphic then + let (inst, subst), ctx = fresh_instance_from mib.mind_universes in + Vars.subst_univs_constr subst oib.mind_arity.mind_user_arity, ctx + else oib.mind_arity.mind_user_arity, ContextSet.empty + | ConstructRef cstr -> + let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + if mib.mind_polymorphic then + let (inst, subst), ctx = fresh_instance_from mib.mind_universes in + Inductive.type_of_constructor (cstr,inst) specif, ctx + else Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty + +let type_of_global t = type_of_reference (Global.env ()) t + +let fresh_sort_in_family env = function + | InProp -> prop_sort, ContextSet.empty + | InSet -> set_sort, ContextSet.empty + | InType -> + let u = fresh_level () in + Type (Univ.Universe.make u), ContextSet.singleton u + +let new_sort_in_family sf = + fst (fresh_sort_in_family (Global.env ()) sf) + +let extend_context (a, ctx) (ctx') = + (a, ContextSet.union ctx ctx') + +let new_global_univ () = + let u = fresh_level () in + (Univ.Universe.make u, ContextSet.singleton u) + +(** Simplification *) + +module LevelUnionFind = Unionfind.Make (Univ.LSet) (Univ.LMap) + +let remove_trivial_constraints cst = + Constraint.fold (fun (l,d,r as cstr) nontriv -> + if d != Lt && eq_levels l r then nontriv + else if d == Le && is_type0m_univ (Univ.Universe.make l) then nontriv + else Constraint.add cstr nontriv) + cst Constraint.empty + +let add_list_map u t map = + let l, d, r = LMap.split u map in + let d' = match d with None -> [t] | Some l -> t :: l in + let lr = + LMap.merge (fun k lm rm -> + match lm with Some t -> lm | None -> + match rm with Some t -> rm | None -> None) l r + in LMap.add u d' lr + +let find_list_map u map = + try LMap.find u map with Not_found -> [] + +module UF = LevelUnionFind +type universe_full_subst = (universe_level * universe) list + +(** Precondition: flexible <= ctx *) +let choose_canonical ctx flexible algs s = + let global = LSet.diff s ctx in + let flexible, rigid = LSet.partition (fun x -> LMap.mem x flexible) (LSet.inter s ctx) in + (** If there is a global universe in the set, choose it *) + if not (LSet.is_empty global) then + let canon = LSet.choose global in + canon, (LSet.remove canon global, rigid, flexible) + else (** No global in the equivalence class, choose a rigid one *) + if not (LSet.is_empty rigid) then + let canon = LSet.choose rigid in + canon, (global, LSet.remove canon rigid, flexible) + else (** There are only flexible universes in the equivalence + class, choose a non-algebraic. *) + let algs, nonalgs = LSet.partition (fun x -> LSet.mem x algs) flexible in + if not (LSet.is_empty nonalgs) then + let canon = LSet.choose nonalgs in + canon, (global, rigid, LSet.remove canon flexible) + else + let canon = LSet.choose algs in + canon, (global, rigid, LSet.remove canon flexible) + +open Universe + +let subst_puniverses subst (c, u as cu) = + let u' = Instance.subst subst u in + if u' == u then cu else (c, u') + +let nf_evars_and_universes_local f subst = + let rec aux c = + match kind_of_term c with + | Evar (evdk, _ as ev) -> + (match f ev with + | None -> c + | Some c -> aux c) + | Const pu -> + let pu' = subst_puniverses subst pu in + if pu' == pu then c else mkConstU pu' + | Ind pu -> + let pu' = subst_puniverses subst pu in + if pu' == pu then c else mkIndU pu' + | Construct pu -> + let pu' = subst_puniverses subst pu in + if pu' == pu then c else mkConstructU pu' + | Sort (Type u) -> + let u' = Univ.subst_univs_level_universe subst u in + if u' == u then c else mkSort (sort_of_univ u') + | _ -> map_constr aux c + in aux + +let subst_univs_fn_puniverses lsubst (c, u as cu) = + let u' = Instance.subst_fn lsubst u in + if u' == u then cu else (c, u') + +let subst_univs_puniverses subst cu = + subst_univs_fn_puniverses (Univ.level_subst_of (Univ.make_subst subst)) cu + +let nf_evars_and_universes_gen f subst = + let lsubst = Univ.level_subst_of subst in + let rec aux c = + match kind_of_term c with + | Evar (evdk, _ as ev) -> + (match try f ev with Not_found -> None with + | None -> c + | Some c -> aux c) + | Const pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkConstU pu' + | Ind pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkIndU pu' + | Construct pu -> + let pu' = subst_univs_fn_puniverses lsubst pu in + if pu' == pu then c else mkConstructU pu' + | Sort (Type u) -> + let u' = Univ.subst_univs_universe subst u in + if u' == u then c else mkSort (sort_of_univ u') + | _ -> map_constr aux c + in aux + +let nf_evars_and_universes_subst f subst = + nf_evars_and_universes_gen f (Univ.make_subst subst) + +let nf_evars_and_universes_opt_subst f subst = + let subst = fun l -> match LMap.find l subst with None -> raise Not_found | Some l' -> l' in + nf_evars_and_universes_gen f subst + +let subst_univs_full_constr subst c = + nf_evars_and_universes_subst (fun _ -> None) subst c + +let fresh_universe_context_set_instance ctx = + if ContextSet.is_empty ctx then LMap.empty, ctx + else + let (univs, cst) = ContextSet.levels ctx, ContextSet.constraints ctx in + let univs',subst = LSet.fold + (fun u (univs',subst) -> + let u' = fresh_level () in + (LSet.add u' univs', LMap.add u u' subst)) + univs (LSet.empty, LMap.empty) + in + let cst' = subst_univs_level_constraints subst cst in + subst, (univs', cst') + +let normalize_univ_variable ~find ~update = + let rec aux cur = + let b = find cur in + let b' = subst_univs_universe aux b in + if Universe.eq b' b then b + else update cur b' + in fun b -> try aux b with Not_found -> Universe.make b + +let normalize_univ_variable_opt_subst ectx = + let find l = + match Univ.LMap.find l !ectx with + | Some b -> b + | None -> raise Not_found + in + let update l b = + assert (match Universe.level b with Some l' -> not (Level.eq l l') | None -> true); + ectx := Univ.LMap.add l (Some b) !ectx; b + in normalize_univ_variable ~find ~update + +let normalize_univ_variable_subst subst = + let find l = Univ.LMap.find l !subst in + let update l b = + assert (match Universe.level b with Some l' -> not (Level.eq l l') | None -> true); + subst := Univ.LMap.add l b !subst; b in + normalize_univ_variable ~find ~update + +let normalize_universe_opt_subst subst = + let normlevel = normalize_univ_variable_opt_subst subst in + subst_univs_universe normlevel + +let normalize_universe_subst subst = + let normlevel = normalize_univ_variable_subst subst in + subst_univs_universe normlevel + +type universe_opt_subst = universe option universe_map + +let make_opt_subst s = + fun x -> + (match Univ.LMap.find x s with + | Some u -> u + | None -> raise Not_found) + +let subst_opt_univs_constr s = + let f = make_opt_subst s in + Vars.subst_univs_fn_constr f + +let normalize_univ_variables ctx = + let ectx = ref ctx in + let normalize = normalize_univ_variable_opt_subst ectx in + let _ = Univ.LMap.iter (fun u _ -> ignore(normalize u)) ctx in + let undef, def, subst = + Univ.LMap.fold (fun u v (undef, def, subst) -> + match v with + | None -> (Univ.LSet.add u undef, def, subst) + | Some b -> (undef, Univ.LSet.add u def, Univ.LMap.add u b subst)) + !ectx (Univ.LSet.empty, Univ.LSet.empty, Univ.LMap.empty) + in !ectx, undef, def, subst + +let pr_universe_body = function + | None -> mt () + | Some v -> str" := " ++ Univ.Universe.pr v + +let pr_universe_opt_subst = Univ.LMap.pr pr_universe_body + +let is_defined_var u l = + try + match LMap.find u l with + | Some _ -> true + | None -> false + with Not_found -> false + +let subst_univs_subst u l s = + LMap.add u l s + +exception Found of Level.t +let find_inst insts v = + try LMap.iter (fun k (enf,alg,v') -> + if not alg && enf && Universe.eq v' v then raise (Found k)) + insts; raise Not_found + with Found l -> l + +let add_inst u (enf,b,lbound) insts = + match lbound with + | Some v -> LMap.add u (enf,b,v) insts + | None -> insts + +exception Stays + +let compute_lbound left = + (** The universe variable was not fixed yet. + Compute its level using its lower bound. *) + if CList.is_empty left then None + else + let lbound = List.fold_left (fun lbound (d, l) -> + if d == Le (* l <= ?u *) then (Universe.sup l lbound) + else (* l < ?u *) + (assert (d == Lt); + (Universe.sup (Universe.super l) lbound))) + Universe.type0m left + in + Some lbound + +let maybe_enforce_leq lbound u cstrs = + match lbound with + | Some lbound -> enforce_leq lbound (Universe.make u) cstrs + | None -> cstrs + +let instantiate_with_lbound u lbound alg enforce (ctx, us, algs, insts, cstrs) = + if enforce then + let inst = Universe.make u in + let cstrs' = enforce_leq lbound inst cstrs in + (ctx, us, LSet.remove u algs, + LMap.add u (enforce,alg,lbound) insts, cstrs'), (enforce, alg, inst) + else (* Actually instantiate *) + (Univ.LSet.remove u ctx, Univ.LMap.add u (Some lbound) us, algs, + LMap.add u (enforce,alg,lbound) insts, cstrs), (enforce, alg, lbound) + +type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t + +let pr_constraints_map cmap = + LMap.fold (fun l cstrs acc -> + Level.pr l ++ str " => " ++ + prlist_with_sep spc (fun (d,r) -> pr_constraint_type d ++ Level.pr r) cstrs ++ fnl () + ++ acc) + cmap (mt ()) + +let minimize_univ_variables ctx us algs left right cstrs = + let left, lbounds = + Univ.LMap.fold (fun r lower (left, lbounds as acc) -> + if Univ.LMap.mem r us || not (Univ.LSet.mem r ctx) then acc + else (* Fixed universe, just compute its glb for sharing *) + let lbounds' = + match compute_lbound (List.map (fun (d,l) -> d, Universe.make l) lower) with + | None -> lbounds + | Some lbound -> LMap.add r (true, false, lbound) lbounds + in (Univ.LMap.remove r left, lbounds')) + left (left, Univ.LMap.empty) + in + let rec instance (ctx', us, algs, insts, cstrs as acc) u = + let acc, left = + try let l = LMap.find u left in + List.fold_left (fun (acc, left') (d, l) -> + let acc', (enf,alg,l') = aux acc l in + (* if alg then assert(not alg); *) + let l' = + if enf then Universe.make l + else l' + (* match Universe.level l' with Some _ -> l' | None -> Universe.make l *) + in + acc', (d, l') :: left') (acc, []) l + with Not_found -> acc, [] + and right = + try Some (LMap.find u right) + with Not_found -> None + in + let instantiate_lbound lbound = + let alg = LSet.mem u algs in + if alg then + (* u is algebraic and has no upper bound constraints: we + instantiate it with it's lower bound, if any *) + instantiate_with_lbound u lbound true false acc + else (* u is non algebraic *) + match Universe.level lbound with + | Some l -> (* The lowerbound is directly a level *) + (* u is not algebraic but has no upper bounds, + we instantiate it with its lower bound if it is a + different level, otherwise we keep it. *) + if not (Level.eq l u) && not (LSet.mem l algs) then + (* if right = None then. Should check that u does not + have upper constraints that are not already in right *) + instantiate_with_lbound u lbound false false acc + (* else instantiate_with_lbound u lbound false true acc *) + else + (* assert false: l can't be alg *) + acc, (true, false, lbound) + | None -> + try + (* if right <> None then raise Not_found; *) + (* Another universe represents the same lower bound, + we can share them with no harm. *) + let can = find_inst insts lbound in + instantiate_with_lbound u (Universe.make can) false false acc + with Not_found -> + (* We set u as the canonical universe representing lbound *) + instantiate_with_lbound u lbound false true acc + in + let acc' acc = + match right with + | None -> acc + | Some cstrs -> + let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in + if List.is_empty dangling then acc + else + let ((ctx', us, algs, insts, cstrs), (enf,_,inst as b)) = acc in + let cstrs' = List.fold_left (fun cstrs (d, r) -> + if d == Univ.Le then + enforce_leq inst (Universe.make r) cstrs + else + try let lev = Option.get (Universe.level inst) in + Constraint.add (lev, d, r) cstrs + with Option.IsNone -> assert false) + cstrs dangling + in + (ctx', us, algs, insts, cstrs'), b + in + if not (LSet.mem u ctx) then acc' (acc, (true, false, Universe.make u)) + else + let lbound = compute_lbound left in + match lbound with + | None -> (* Nothing to do *) + acc' (acc, (true, false, Universe.make u)) + | Some lbound -> + acc' (instantiate_lbound lbound) + and aux (ctx', us, algs, seen, cstrs as acc) u = + try acc, LMap.find u seen + with Not_found -> instance acc u + in + LMap.fold (fun u v (ctx', us, algs, seen, cstrs as acc) -> + if v == None then fst (aux acc u) + else LSet.remove u ctx', us, LSet.remove u algs, seen, cstrs) + us (ctx, us, algs, lbounds, cstrs) + +let normalize_context_set ctx us algs = + let (ctx, csts) = ContextSet.levels ctx, ContextSet.constraints ctx in + let uf = UF.create () in + let csts = + (* We first put constraints in a normal-form: all self-loops are collapsed + to equalities. *) + let g = Univ.merge_constraints csts Univ.empty_universes in + Univ.constraints_of_universes (Univ.normalize_universes g) + in + let noneqs = + Constraint.fold (fun (l,d,r) noneqs -> + if d == Eq then (UF.union l r uf; noneqs) + else Constraint.add (l,d,r) noneqs) + csts Constraint.empty + in + let partition = UF.partition uf in + let subst, eqs = List.fold_left (fun (subst, cstrs) s -> + let canon, (global, rigid, flexible) = choose_canonical ctx us algs s in + (* Add equalities for globals which can't be merged anymore. *) + let cstrs = LSet.fold (fun g cst -> + Constraint.add (canon, Univ.Eq, g) cst) global cstrs + in + (** Should this really happen? *) + let subst' = LSet.fold (fun f -> LMap.add f canon) + (LSet.union rigid flexible) LMap.empty + in + let subst = LMap.union subst' subst in + (subst, cstrs)) + (LMap.empty, Constraint.empty) partition + in + (* Noneqs is now in canonical form w.r.t. equality constraints, + and contains only inequality constraints. *) + let noneqs = subst_univs_level_constraints subst noneqs in + let us = + LMap.subst_union (LMap.map (fun v -> Some (Universe.make v)) subst) us + in + (* Compute the left and right set of flexible variables, constraints + mentionning other variables remain in noneqs. *) + let noneqs, ucstrsl, ucstrsr = + Constraint.fold (fun (l,d,r as cstr) (noneq, ucstrsl, ucstrsr) -> + let lus = LMap.mem l us + and rus = LMap.mem r us + in + let ucstrsl' = + if lus then add_list_map l (d, r) ucstrsl + else ucstrsl + and ucstrsr' = + add_list_map r (d, l) ucstrsr + in + let noneqs = + if lus || rus then noneq + else Constraint.add cstr noneq + in (noneqs, ucstrsl', ucstrsr')) + noneqs (Constraint.empty, LMap.empty, LMap.empty) + in + (* Now we construct the instanciation of each variable. *) + let ctx', us, algs, inst, noneqs = + minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs + in + let us = ref us in + let norm = normalize_univ_variable_opt_subst us in + let _normalize_subst = LMap.iter (fun u v -> ignore(norm u)) !us in + (!us, algs), (ctx', Constraint.union noneqs eqs) + +(* let normalize_conkey = Profile.declare_profile "normalize_context_set" *) +(* let normalize_context_set a b c = Profile.profile3 normalize_conkey normalize_context_set a b c *) + +let universes_of_constr c = + let rec aux s c = + match kind_of_term c with + | Const (_, u) | Ind (_, u) | Construct (_, u) -> + LSet.union (Instance.levels u) s + | Sort u -> + let u = univ_of_sort u in + LSet.union (Universe.levels u) s + | _ -> fold_constr aux s c + in aux LSet.empty c + +let shrink_universe_context (univs,csts) s = + let univs' = LSet.inter univs s in + Constraint.fold (fun (l,d,r as c) (univs',csts) -> + if LSet.mem l univs' then + let univs' = if LSet.mem r univs then LSet.add r univs' else univs' in + (univs', Constraint.add c csts) + else if LSet.mem r univs' then + let univs' = if LSet.mem l univs then LSet.add l univs' else univs' in + (univs', Constraint.add c csts) + else (univs', csts)) + csts (univs',Constraint.empty) + +let restrict_universe_context (univs,csts) s = + let univs' = LSet.inter univs s in + (* Universes that are not necessary to typecheck the term. + E.g. univs introduced by tactics and not used in the proof term. *) + let diff = LSet.diff univs s in + let csts' = + Constraint.fold (fun (l,d,r as c) csts -> + if LSet.mem l diff || LSet.mem r diff then csts + else Constraint.add c csts) + csts Constraint.empty + in (univs', csts') + +let is_prop_leq (l,d,r) = + Level.eq Level.prop l && d == Univ.Le + +(* Prop < i <-> Set+1 <= i <-> Set < i *) +let translate_cstr (l,d,r as cstr) = + if Level.eq Level.prop l && d == Univ.Lt then + (Level.set, d, r) + else cstr + +let refresh_constraints univs (ctx, cstrs) = + let cstrs', univs' = + Univ.Constraint.fold (fun c (cstrs', univs as acc) -> + let c = translate_cstr c in + if Univ.check_constraint univs c && not (is_prop_leq c) then acc + else (Univ.Constraint.add c cstrs', Univ.enforce_constraint c univs)) + cstrs (Univ.Constraint.empty, univs) + in ((ctx, cstrs'), univs') + +let remove_trivial_constraints (ctx, cstrs) = + let cstrs' = + Univ.Constraint.fold (fun c acc -> + if is_prop_leq c then Univ.Constraint.remove c acc + else acc) cstrs cstrs + in (ctx, cstrs') diff --git a/library/universes.mli b/library/universes.mli new file mode 100644 index 000000000..47876269a --- /dev/null +++ b/library/universes.mli @@ -0,0 +1,170 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Pp +open Names +open Term +open Context +open Environ +open Locus +open Univ + +(** Universes *) +val new_univ_level : Names.dir_path -> universe_level +val set_remote_new_univ_level : universe_level RemoteCounter.installer +val new_univ : Names.dir_path -> universe +val new_Type : Names.dir_path -> types +val new_Type_sort : Names.dir_path -> sorts + +(** Build a fresh instance for a given context, its associated substitution and + the instantiated constraints. *) + +val fresh_instance_from_context : universe_context -> + (universe_instance * universe_subst) constrained + +val fresh_instance_from : universe_context -> + (universe_instance * universe_subst) in_universe_context_set + +val new_global_univ : unit -> universe in_universe_context_set +val new_sort_in_family : sorts_family -> sorts + +val fresh_sort_in_family : env -> sorts_family -> + sorts in_universe_context_set +val fresh_constant_instance : env -> constant -> + pconstant in_universe_context_set +val fresh_inductive_instance : env -> inductive -> + pinductive in_universe_context_set +val fresh_constructor_instance : env -> constructor -> + pconstructor in_universe_context_set + +val fresh_global_instance : env -> Globnames.global_reference -> + constr in_universe_context_set + +val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> + constr in_universe_context_set + +(** Raises [Not_found] if not a global reference. *) +val global_of_constr : constr -> Globnames.global_reference puniverses + +val global_app_of_constr : constr -> Globnames.global_reference puniverses * constr option + +val constr_of_global_univ : Globnames.global_reference puniverses -> constr + +val extend_context : 'a in_universe_context_set -> universe_context_set -> + 'a in_universe_context_set + +(** Simplification and pruning of constraints: + [normalize_context_set ctx us] + + - Instantiate the variables in [us] with their most precise + universe levels respecting the constraints. + + - Normalizes the context [ctx] w.r.t. equality constraints, + choosing a canonical universe in each equivalence class + (a global one if there is one) and transitively saturate + the constraints w.r.t to the equalities. *) + +module UF : Unionfind.PartitionSig with type elt = universe_level + +type universe_opt_subst = universe option universe_map + +val make_opt_subst : universe_opt_subst -> universe_subst_fn + +val subst_opt_univs_constr : universe_opt_subst -> constr -> constr + +val choose_canonical : universe_set -> universe_opt_subst -> universe_set -> universe_set -> + universe_level * (universe_set * universe_set * universe_set) + +val instantiate_with_lbound : + Univ.LMap.key -> + Univ.universe -> + bool -> + bool -> + Univ.LSet.t * Univ.universe option Univ.LMap.t * + Univ.LSet.t * + (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints -> + (Univ.LSet.t * Univ.universe option Univ.LMap.t * + Univ.LSet.t * + (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints) * + (bool * bool * Univ.universe) + +val compute_lbound : (constraint_type * Univ.universe) list -> universe option + +type constraints_map = (Univ.constraint_type * Univ.LMap.key) list Univ.LMap.t + +val pr_constraints_map : constraints_map -> Pp.std_ppcmds + +val minimize_univ_variables : + Univ.LSet.t -> + Univ.universe option Univ.LMap.t -> + Univ.LSet.t -> + constraints_map -> constraints_map -> + Univ.constraints -> + Univ.LSet.t * Univ.universe option Univ.LMap.t * + Univ.LSet.t * + (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints + + +val normalize_context_set : universe_context_set -> + universe_opt_subst (* The defined and undefined variables *) -> + universe_set (* univ variables that can be substituted by algebraics *) -> + (universe_opt_subst * universe_set) in_universe_context_set + +val normalize_univ_variables : universe_opt_subst -> + universe_opt_subst * universe_set * universe_set * universe_subst + +val normalize_univ_variable : + find:(universe_level -> universe) -> + update:(universe_level -> universe -> universe) -> + universe_level -> universe + +val normalize_univ_variable_opt_subst : universe_opt_subst ref -> + (universe_level -> universe) + +val normalize_univ_variable_subst : universe_subst ref -> + (universe_level -> universe) + +val normalize_universe_opt_subst : universe_opt_subst ref -> + (universe -> universe) + +val normalize_universe_subst : universe_subst ref -> + (universe -> universe) + +(** Create a fresh global in the global environment, shouldn't be done while + building polymorphic values as the constraints are added to the global + environment already. *) + +val constr_of_global : Globnames.global_reference -> constr + +val type_of_global : Globnames.global_reference -> types in_universe_context_set + +(** Full universes substitutions into terms *) + +val nf_evars_and_universes_local : (existential -> constr option) -> universe_level_subst -> + constr -> constr + +val nf_evars_and_universes_opt_subst : (existential -> constr option) -> + universe_opt_subst -> constr -> constr + +(** Get fresh variables for the universe context. + Useful to make tactics that manipulate constrs in universe contexts polymorphic. *) +val fresh_universe_context_set_instance : universe_context_set -> + universe_level_subst * universe_context_set + +val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds + +(** Shrink a universe context to a restricted set of variables *) + +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 refresh_constraints : universes -> universe_context_set -> universe_context_set * universes + +val remove_trivial_constraints : universe_context_set -> universe_context_set |