diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 13 | ||||
| -rw-r--r-- | engine/eConstr.mli | 4 | ||||
| -rw-r--r-- | engine/engine.mllib | 2 | ||||
| -rw-r--r-- | engine/evarutil.ml | 31 | ||||
| -rw-r--r-- | engine/evarutil.mli | 14 | ||||
| -rw-r--r-- | engine/evd.ml | 139 | ||||
| -rw-r--r-- | engine/evd.mli | 39 | ||||
| -rw-r--r-- | engine/namegen.ml | 13 | ||||
| -rw-r--r-- | engine/proofview.ml | 58 | ||||
| -rw-r--r-- | engine/proofview.mli | 9 | ||||
| -rw-r--r-- | engine/termops.ml | 52 | ||||
| -rw-r--r-- | engine/termops.mli | 2 | ||||
| -rw-r--r-- | engine/uState.ml | 15 | ||||
| -rw-r--r-- | engine/uState.mli | 11 | ||||
| -rw-r--r-- | engine/univGen.ml | 212 | ||||
| -rw-r--r-- | engine/univGen.mli | 24 | ||||
| -rw-r--r-- | engine/univNames.ml | 2 | ||||
| -rw-r--r-- | engine/univops.ml | 28 | ||||
| -rw-r--r-- | engine/univops.mli | 6 |
19 files changed, 351 insertions, 323 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 8ab3ce821e..3385b78958 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -74,6 +74,12 @@ let mkCoFix f = of_kind (CoFix f) let mkProj (p, c) = of_kind (Proj (p, c)) let mkArrow t1 t2 = of_kind (Prod (Anonymous, t1, t2)) +let mkRef (gr,u) = let open GlobRef in match gr with + | ConstRef c -> mkConstU (c,u) + | IndRef ind -> mkIndU (ind,u) + | ConstructRef c -> mkConstructU (c,u) + | VarRef x -> mkVar x + let applist (f, arg) = mkApp (f, Array.of_list arg) let isRel sigma c = match kind sigma c with Rel _ -> true | _ -> false @@ -166,6 +172,13 @@ let destProj sigma c = match kind sigma c with | Proj (p, c) -> (p, c) | _ -> raise DestKO +let destRef sigma c = let open GlobRef in match kind sigma c with + | Var x -> VarRef x, EInstance.empty + | Const (c,u) -> ConstRef c, u + | Ind (ind,u) -> IndRef ind, u + | Construct (c,u) -> ConstructRef c, u + | _ -> raise DestKO + let decompose_app sigma c = match kind sigma c with | App (f,cl) -> (f, Array.to_list cl) diff --git a/engine/eConstr.mli b/engine/eConstr.mli index f897448557..1edc0ee12b 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -122,6 +122,8 @@ val mkFix : (t, t) pfixpoint -> t val mkCoFix : (t, t) pcofixpoint -> t val mkArrow : t -> t -> t +val mkRef : GlobRef.t * EInstance.t -> t + val applist : t * t list -> t val mkProd_or_LetIn : rel_declaration -> t -> t @@ -180,6 +182,8 @@ val destProj : Evd.evar_map -> t -> Projection.t * t val destFix : Evd.evar_map -> t -> (t, t) pfixpoint val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint +val destRef : Evd.evar_map -> t -> GlobRef.t * EInstance.t + val decompose_app : Evd.evar_map -> t -> t * t list (** Pops lambda abstractions until there are no more, skipping casts. *) diff --git a/engine/engine.mllib b/engine/engine.mllib index 37e83b6238..bb43808542 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -4,8 +4,8 @@ UnivSubst UnivProblem UnivMinim Universes -Univops UState +Univops Nameops Evar_kinds Evd diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 13356627f0..4e1636e321 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -405,12 +405,13 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ = let default_source = Loc.tag @@ Evar_kinds.InternalHole -let new_pure_evar_full evd evi = - let (evd, evk) = Evd.new_evar evd evi in +let new_pure_evar_full evd ?typeclass_candidate evi = + let (evd, evk) = Evd.new_evar evd ?typeclass_candidate evi in let evd = Evd.declare_future_goal evk evd in (evd, evk) -let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ = +let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?typeclass_candidate + ?(principal=false) sign evd typ = let default_naming = IntroAnonymous in let naming = Option.default default_naming naming in let name = match naming with @@ -427,34 +428,34 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ? evar_body = Evar_empty; evar_filter = filter; evar_source = src; - evar_candidates = candidates; - evar_extra = store; } + evar_candidates = candidates } in - let (evd, newevk) = Evd.new_evar evd ?name evi in + let typeclass_candidate = if principal then Some false else typeclass_candidate in + let (evd, newevk) = Evd.new_evar evd ?name ?typeclass_candidate evi in let evd = if principal then Evd.declare_principal_goal newevk evd else Evd.declare_future_goal newevk evd in (evd, newevk) -let new_evar_instance ?src ?filter ?candidates ?store ?naming ?principal sign evd typ instance = +let new_evar_instance ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ instance = let open EConstr in assert (not !Flags.debug || List.distinct (ids_of_named_context (named_context_of_val sign))); - let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in + let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal typ in evd, mkEvar (newevk,Array.of_list instance) -let new_evar_from_context ?src ?filter ?candidates ?store ?naming ?principal sign evd typ = +let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ = let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in let instance = match filter with | None -> instance | Some filter -> Filter.filter_list filter instance in - new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance + new_evar_instance sign evd typ ?src ?filter ?candidates ?naming ?principal instance (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env evd typ = +let new_evar ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal ?hypnaming env evd typ = let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in let map c = csubst_subst subst c in let candidates = Option.map (fun l -> List.map map l) candidates in @@ -462,11 +463,11 @@ let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env e match filter with | None -> instance | Some filter -> Filter.filter_list filter instance in - new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance + new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal instance let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid = let (evd', s) = new_sort_variable rigid evd in - let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in + let (evd', e) = new_evar env evd' ?src ?filter ?naming ~typeclass_candidate:false ?principal ?hypnaming (EConstr.mkSort s) in evd', (e, s) let new_Type ?(rigid=Evd.univ_flexible) evd = @@ -549,7 +550,7 @@ let rec check_and_clear_in_constr env evdref err ids global c = if Id.Set.mem id' ids then raise (ClearDependencyError (id',err,Some (Globnames.global_of_constr c))) in - Id.Set.iter check (Environ.vars_of_global env c) + Id.Set.iter check (Environ.vars_of_global env (fst @@ destRef c)) in c @@ -714,7 +715,7 @@ let rec advance sigma evk = match evi.evar_body with | Evar_empty -> Some evk | Evar_defined v -> - match is_restricted_evar evi with + match is_restricted_evar sigma evk with | Some evk -> advance sigma evk | None -> None diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 11e07175e3..0c8d8c9b8a 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -27,8 +27,9 @@ val mk_new_meta : unit -> constr val new_evar_from_context : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> + ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> + ?typeclass_candidate:bool -> ?principal:bool -> named_context_val -> evar_map -> types -> evar_map * EConstr.t @@ -40,19 +41,21 @@ type naming_mode = val new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> + ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> + ?typeclass_candidate:bool -> ?principal:bool -> ?hypnaming:naming_mode -> env -> evar_map -> types -> evar_map * EConstr.t val new_pure_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> + ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> + ?typeclass_candidate:bool -> ?principal:bool -> named_context_val -> evar_map -> types -> evar_map * Evar.t -val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t +val new_pure_evar_full : evar_map -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) @@ -77,7 +80,8 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr as a telescope) is [sign] *) val new_evar_instance : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> - ?store:Store.t -> ?naming:intro_pattern_naming_expr -> + ?naming:intro_pattern_naming_expr -> + ?typeclass_candidate:bool -> ?principal:bool -> named_context_val -> evar_map -> types -> constr list -> evar_map * constr diff --git a/engine/evd.ml b/engine/evd.ml index d7b03a84f1..3a77a2b440 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -144,8 +144,7 @@ type evar_info = { evar_body : evar_body; evar_filter : Filter.t; evar_source : Evar_kinds.t Loc.located; - evar_candidates : constr list option; (* if not None, list of allowed instances *) - evar_extra : Store.t } + evar_candidates : constr list option; (* if not None, list of allowed instances *)} let make_evar hyps ccl = { evar_concl = ccl; @@ -153,9 +152,7 @@ let make_evar hyps ccl = { evar_body = Evar_empty; evar_filter = Filter.identity; evar_source = Loc.tag @@ Evar_kinds.InternalHole; - evar_candidates = None; - evar_extra = Store.empty -} + evar_candidates = None; } let instance_mismatch () = anomaly (Pp.str "Signature and its instance do not match.") @@ -413,6 +410,11 @@ end type goal_kind = ToShelve | ToGiveUp +type evar_flags = + { obligation_evars : Evar.Set.t; + restricted_evars : Evar.t Evar.Map.t; + typeclass_evars : Evar.Set.t } + type evar_map = { (** Existential variables *) defn_evars : evar_info EvMap.t; @@ -425,6 +427,7 @@ type evar_map = { last_mods : Evar.Set.t; (** Metas *) metas : clbinding Metamap.t; + evar_flags : evar_flags; (** Interactive proofs *) effects : Safe_typing.private_constants; future_goals : Evar.t list; (** list of newly created evars, to be @@ -441,20 +444,82 @@ type evar_map = { extras : Store.t; } +let get_is_maybe_typeclass, (is_maybe_typeclass_hook : (evar_map -> constr -> bool) Hook.t) = Hook.make ~default:(fun evd c -> false) () + +let is_maybe_typeclass sigma c = Hook.get get_is_maybe_typeclass sigma c + (*** Lifting primitive from Evar.Map. ***) let rename evk id evd = { evd with evar_names = EvNames.rename evk id evd.evar_names } -let add_with_name ?name d e i = match i.evar_body with +let add_with_name ?name ?(typeclass_candidate = true) d e i = match i.evar_body with | Evar_empty -> let evar_names = EvNames.add_name_undefined name e i d.evar_names in - { d with undf_evars = EvMap.add e i d.undf_evars; evar_names } + let evar_flags = + if typeclass_candidate && is_maybe_typeclass d i.evar_concl then + let flags = d.evar_flags in + { flags with typeclass_evars = Evar.Set.add e flags.typeclass_evars } + else d.evar_flags + in + { d with undf_evars = EvMap.add e i d.undf_evars; evar_names; evar_flags } | Evar_defined _ -> let evar_names = EvNames.remove_name_defined e d.evar_names in { d with defn_evars = EvMap.add e i d.defn_evars; evar_names } -let add d e i = add_with_name d e i +(** Evd.add is a low-level function mainly used to update the evar_info + associated to an evar, so we prevent registering its typeclass status. *) +let add d e i = add_with_name ~typeclass_candidate:false d e i + +(*** Evar flags: typeclasses, restricted or obligation flag *) + +let get_typeclass_evars evd = evd.evar_flags.typeclass_evars + +let set_typeclass_evars evd tcs = + let flags = evd.evar_flags in + { evd with evar_flags = { flags with typeclass_evars = tcs } } + +let is_typeclass_evar evd evk = + let flags = evd.evar_flags in + Evar.Set.mem evk flags.typeclass_evars + +let set_obligation_evar evd evk = + let flags = evd.evar_flags in + let evar_flags = { flags with obligation_evars = Evar.Set.add evk flags.obligation_evars } in + { evd with evar_flags } + +let is_obligation_evar evd evk = + let flags = evd.evar_flags in + Evar.Set.mem evk flags.obligation_evars + +(** Inheritance of flags: for evar-evar and restriction cases *) + +let inherit_evar_flags evar_flags evk evk' = + let evk_typeclass = Evar.Set.mem evk evar_flags.typeclass_evars in + let evk_obligation = Evar.Set.mem evk evar_flags.obligation_evars in + if not (evk_obligation || evk_typeclass) then evar_flags + else + let typeclass_evars = + if evk_typeclass then + let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in + Evar.Set.add evk' typeclass_evars + else evar_flags.typeclass_evars + in + let obligation_evars = + if evk_obligation then + let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in + Evar.Set.add evk' obligation_evars + else evar_flags.obligation_evars + in + { evar_flags with obligation_evars; typeclass_evars } + +(** Removal: in all other cases of definition *) + +let remove_evar_flags evk evar_flags = + { typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars; + obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars; + (** Restriction information is kept. *) + restricted_evars = evar_flags.restricted_evars } (** New evars *) @@ -464,9 +529,9 @@ let evar_counter_summary_name = "evar counter" let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name let new_untyped_evar () = incr evar_ctr; Evar.unsafe_of_int !evar_ctr -let new_evar evd ?name evi = +let new_evar evd ?name ?typeclass_candidate evi = let evk = new_untyped_evar () in - let evd = add_with_name evd ?name evk evi in + let evd = add_with_name evd ?name ?typeclass_candidate evk evi in (evd, evk) let remove d e = @@ -478,7 +543,9 @@ let remove d e = in let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in let future_goals_status = EvMap.remove e d.future_goals_status in - { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status } + let evar_flags = remove_evar_flags e d.evar_flags in + { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status; + evar_flags } let find d e = try EvMap.find e d.undf_evars @@ -583,12 +650,18 @@ let cmap f evd = let create_evar_defs sigma = { sigma with conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty } +let empty_evar_flags = + { obligation_evars = Evar.Set.empty; + restricted_evars = Evar.Map.empty; + typeclass_evars = Evar.Set.empty } + let empty = { defn_evars = EvMap.empty; undf_evars = EvMap.empty; universes = UState.empty; conv_pbs = []; last_mods = Evar.Set.empty; + evar_flags = empty_evar_flags; metas = Metamap.empty; effects = Safe_typing.empty_private_constants; evar_names = EvNames.empty; (* id<->key for undefined evars *) @@ -634,9 +707,7 @@ let evar_source evk d = (find d evk).evar_source let evar_ident evk evd = EvNames.ident evk evd.evar_names let evar_key id evd = EvNames.key id evd.evar_names -let restricted = Store.field () - -let define_aux ?dorestrict def undef evk body = +let define_aux def undef evk body = let oldinfo = try EvMap.find evk undef with Not_found -> @@ -646,24 +717,39 @@ let define_aux ?dorestrict def undef evk body = anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.") in let () = assert (oldinfo.evar_body == Evar_empty) in - let evar_extra = match dorestrict with - | Some evk' -> Store.set oldinfo.evar_extra restricted evk' - | None -> oldinfo.evar_extra in - let newinfo = { oldinfo with evar_body = Evar_defined body; evar_extra } in + let newinfo = { oldinfo with evar_body = Evar_defined body } in EvMap.add evk newinfo def, EvMap.remove evk undef (* define the existential of section path sp as the constr body *) -let define evk body evd = +let define_gen evk body evd evar_flags = let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in let last_mods = match evd.conv_pbs with | [] -> evd.last_mods | _ -> Evar.Set.add evk evd.last_mods in let evar_names = EvNames.remove_name_defined evk evd.evar_names in - { evd with defn_evars; undf_evars; last_mods; evar_names } + { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags } -let is_restricted_evar evi = - Store.get evi.evar_extra restricted +(** By default, the obligation and evar tag of the evar is removed *) +let define evk body evd = + let evar_flags = remove_evar_flags evk evd.evar_flags in + define_gen evk body evd evar_flags + +(** In case of an evar-evar solution, the flags are inherited *) +let define_with_evar evk body evd = + let evk' = fst (destEvar body) in + let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in + define_gen evk body evd evar_flags + +let is_restricted_evar evd evk = + try Some (Evar.Map.find evk evd.evar_flags.restricted_evars) + with Not_found -> None + +let declare_restricted_evar evar_flags evk evk' = + { evar_flags with restricted_evars = Evar.Map.add evk evk' evar_flags.restricted_evars } + +(* In case of restriction, we declare the restriction and inherit the obligation + and typeclass flags. *) let restrict evk filter ?candidates ?src evd = let evk' = new_untyped_evar () in @@ -679,9 +765,11 @@ let restrict evk filter ?candidates ?src evd = let ctxt = Filter.filter_list filter (evar_context evar_info) in let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in let body = mkEvar(evk',id_inst) in - let (defn_evars, undf_evars) = define_aux ~dorestrict:evk' evd.defn_evars evd.undf_evars evk body in + let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in + let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in + let evar_flags = inherit_evar_flags evar_flags evk evk' in { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; - defn_evars; last_mods; evar_names }, evk' + defn_evars; last_mods; evar_names; evar_flags }, evk' let downcast evk ccl evd = let evar_info = EvMap.find evk evd.undf_evars in @@ -818,7 +906,7 @@ let fresh_constructor_instance ?loc env evd c = with_context_set ?loc univ_flexible evd (UnivGen.fresh_constructor_instance env c) let fresh_global ?loc ?(rigid=univ_flexible) ?names env evd gr = - with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?names env gr) + with_context_set ?loc rigid evd (UnivGen.fresh_global_instance ?loc ?names env gr) let is_sort_variable evd s = UState.is_sort_variable evd.universes s @@ -1019,6 +1107,7 @@ let set_metas evd metas = { universes = evd.universes; conv_pbs = evd.conv_pbs; last_mods = evd.last_mods; + evar_flags = evd.evar_flags; metas; effects = evd.effects; evar_names = evd.evar_names; diff --git a/engine/evd.mli b/engine/evd.mli index 1a5614988d..b0e3c2b869 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -83,10 +83,6 @@ type evar_body = | Evar_empty | Evar_defined of econstr - -module Store : Store.S -(** Datatype used to store additional information in evar maps. *) - type evar_info = { evar_concl : econstr; (** Type of the evar. *) @@ -102,8 +98,6 @@ type evar_info = { (** Information about the evar. *) evar_candidates : econstr list option; (** List of possible solutions when known that it is a finite list *) - evar_extra : Store.t - (** Extra store, used for clever hacks. *) } val make_evar : named_context_val -> etypes -> evar_info @@ -145,7 +139,7 @@ val has_undefined : evar_map -> bool there are uninstantiated evars in [sigma]. *) val new_evar : evar_map -> - ?name:Id.t -> evar_info -> evar_map * Evar.t + ?name:Id.t -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t (** Creates a fresh evar mapping to the given information. *) val add : evar_map -> Evar.t -> evar_info -> evar_map @@ -182,7 +176,7 @@ val raw_map_undefined : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_m (** Same as {!raw_map}, but restricted to undefined evars. For efficiency reasons. *) -val define : Evar.t-> econstr -> evar_map -> evar_map +val define : Evar.t -> econstr -> evar_map -> evar_map (** Set the body of an evar to the given constr. It is expected that: {ul {- The evar is already present in the evarmap.} @@ -190,6 +184,10 @@ val define : Evar.t-> econstr -> evar_map -> evar_map {- All the evars present in the constr should be present in the evar map.} } *) +val define_with_evar : Evar.t -> econstr -> evar_map -> evar_map +(** Same as [define ev body evd], except the body must be an existential variable [ev']. + This additionally makes [ev'] inherit the [obligation] and [typeclass] flags of [ev]. *) + val cmap : (econstr -> econstr) -> evar_map -> evar_map (** Map the function on all terms in the evar map. *) @@ -210,6 +208,8 @@ val undefined_map : evar_map -> evar_info Evar.Map.t val drop_all_defined : evar_map -> evar_map +val is_maybe_typeclass_hook : (evar_map -> constr -> bool) Hook.t + (** {6 Instantiating partial terms} *) exception NotInstantiatedEvar @@ -247,9 +247,27 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list -> possibly limiting the instances to a set of candidates (candidates are filtered according to the filter) *) -val is_restricted_evar : evar_info -> Evar.t option +val is_restricted_evar : evar_map -> Evar.t -> Evar.t option (** Tell if an evar comes from restriction of another evar, and if yes, which *) +val set_typeclass_evars : evar_map -> Evar.Set.t -> evar_map +(** Mark the given set of evars as available for resolution. + + Precondition: they should indeed refer to undefined typeclass evars. + *) + +val get_typeclass_evars : evar_map -> Evar.Set.t +(** The set of undefined typeclass evars *) + +val is_typeclass_evar : evar_map -> Evar.t -> bool +(** Is the evar declared resolvable for typeclass resolution *) + +val set_obligation_evar : evar_map -> Evar.t -> evar_map +(** Declare an evar as an obligation *) + +val is_obligation_evar : evar_map -> Evar.t -> bool +(** Is the evar declared as an obligation *) + val downcast : Evar.t-> etypes -> evar_map -> evar_map (** Change the type of an undefined evar to a new type assumed to be a subtype of its current type; subtyping must be ensured by caller *) @@ -357,6 +375,9 @@ val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map *) +module Store : Store.S +(** Datatype used to store additional information in evar maps. *) + val get_extra_data : evar_map -> Store.t val set_extra_data : Store.t -> evar_map -> evar_map diff --git a/engine/namegen.ml b/engine/namegen.ml index 7ce759a3fb..db72dc8ec3 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -21,7 +21,6 @@ open Constr open Environ open EConstr open Vars -open Nametab open Nameops open Libnames open Globnames @@ -82,14 +81,14 @@ let is_imported_ref = function let is_global id = try - let ref = locate (qualid_of_ident id) in + let ref = Nametab.locate (qualid_of_ident id) in not (is_imported_ref ref) with Not_found -> false let is_constructor id = try - match locate (qualid_of_ident id) with + match Nametab.locate (qualid_of_ident id) with | ConstructRef _ -> true | _ -> false with Not_found -> @@ -116,7 +115,7 @@ let head_name sigma c = (* Find the head constant of a constr if any *) | Cast (c,_,_) | App (c,_) -> hdrec c | Proj (kn,_) -> Some (Label.to_id (Constant.label (Projection.constant kn))) | Const _ | Ind _ | Construct _ | Var _ as c -> - Some (basename_of_global (global_of_constr c)) + Some (Nametab.basename_of_global (global_of_constr c)) | Fix ((_,i),(lna,_,_)) | CoFix (i,(lna,_,_)) -> Some (match lna.(i) with Name id -> id | _ -> assert false) | Sort _ | Rel _ | Meta _|Evar _|Case (_, _, _, _) -> None @@ -148,8 +147,8 @@ let hdchar env sigma c = | Cast (c,_,_) | App (c,_) -> hdrec k c | Proj (kn,_) -> lowercase_first_char (Label.to_id (Constant.label (Projection.constant kn))) | Const (kn,_) -> lowercase_first_char (Label.to_id (Constant.label kn)) - | Ind (x,_) -> (try lowercase_first_char (basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") - | Construct (x,_) -> (try lowercase_first_char (basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Ind (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (IndRef x)) with Not_found when !Flags.in_debugger -> "zz") + | Construct (x,_) -> (try lowercase_first_char (Nametab.basename_of_global (ConstructRef x)) with Not_found when !Flags.in_debugger -> "zz") | Var id -> lowercase_first_char id | Sort s -> sort_hdchar (ESorts.kind sigma s) | Rel n -> @@ -267,7 +266,7 @@ let visible_ids sigma (nenv, c) = begin try let gseen = GlobRef.Set_env.add g gseen in - let short = shortest_qualid_of_global Id.Set.empty g in + let short = Nametab.shortest_qualid_of_global Id.Set.empty g in let dir, id = repr_qualid short in let ids = if DirPath.is_empty dir then Id.Set.add id ids else ids in accu := (gseen, vseen, ids) diff --git a/engine/proofview.ml b/engine/proofview.ml index 12d31e5f46..304b2dff84 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -60,19 +60,14 @@ type telescope = | TNil of Evd.evar_map | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope) -let typeclass_resolvable = Evd.Store.field () - let dependent_init = - (* Goals are created with a store which marks them as unresolvable - for type classes. *) - let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () in (* Goals don't have a source location. *) let src = Loc.tag @@ Evar_kinds.GoalEvar in (* Main routine *) let rec aux = function | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] } | TCons (env, sigma, typ, t) -> - let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~store typ in + let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~typeclass_candidate:false typ in let (gl, _) = EConstr.destEvar sigma econstr in let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in let entry = (econstr, typ) :: ret in @@ -745,26 +740,28 @@ let unshelve l p = let l = undefined p.solution l in { p with comb = p.comb@l } -let mark_in_evm ~goal evd content = - let info = Evd.find evd content in - let info = +let mark_in_evm ~goal evd evars = + let evd = if goal then - { info with Evd.evar_source = match info.Evd.evar_source with - (* Two kinds for goal evars: - - GoalEvar (morally not dependent) - - VarInstance (morally dependent of some name). - This is a heuristic for naming these evars. *) - | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} | - Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id - | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x - | loc,_ -> loc,Evar_kinds.GoalEvar } - else info - in - let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with - | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () } - | Some () -> info + let mark evd content = + let info = Evd.find evd content in + let info = + { info with Evd.evar_source = match info.Evd.evar_source with + (* Two kinds for goal evars: + - GoalEvar (morally not dependent) + - VarInstance (morally dependent of some name). + This is a heuristic for naming these evars. *) + | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} | + Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id + | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x + | loc,_ -> loc,Evar_kinds.GoalEvar } + in Evd.add evd content info + in CList.fold_left mark evd evars + else evd in - Evd.add evd content info + let tcs = Evd.get_typeclass_evars evd in + let evset = Evar.Set.of_list evars in + Evd.set_typeclass_evars evd (Evar.Set.diff tcs evset) let with_shelf tac = let open Proof in @@ -781,7 +778,7 @@ let with_shelf tac = let sigma = Evd.restore_future_goals sigma fgoals in (* Ensure we mark and return only unsolved goals *) let gls' = undefined_evars sigma (CList.rev_append gls' gls) in - let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in + let sigma = mark_in_evm ~goal:false sigma gls' in let npv = { npv with shelf; solution = sigma } in Pv.set npv >> tclUNIT (gls', ans) @@ -1035,7 +1032,7 @@ module Unsafe = struct let reset_future_goals p = { p with solution = Evd.reset_future_goals p.solution } - let mark_as_goal evd content = + let mark_as_goals evd content = mark_in_evm ~goal:true evd content let advance = Evarutil.advance @@ -1043,9 +1040,7 @@ module Unsafe = struct let undefined = undefined let mark_as_unresolvable p gl = - { p with solution = mark_in_evm ~goal:false p.solution gl } - - let typeclass_resolvable = typeclass_resolvable + { p with solution = mark_in_evm ~goal:false p.solution [gl] } end @@ -1065,10 +1060,6 @@ let goal_nf_evar sigma gl = let sigma = Evd.add sigma gl evi in (gl, sigma) -let goal_extra evars gl = - let evi = Evd.find evars gl in - evi.Evd.evar_extra - let catchable_exception = function | Logic_monad.Exception _ -> false @@ -1093,7 +1084,6 @@ module Goal = struct let sigma {sigma} = sigma let hyps {env} = EConstr.named_context env let concl {concl} = concl - let extra {sigma; self} = goal_extra sigma self let gmake_with info env sigma goal state = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; diff --git a/engine/proofview.mli b/engine/proofview.mli index 0bb3229a9b..cda4808a23 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -456,9 +456,9 @@ module Unsafe : sig (** Clears the future goals store in the proof view. *) val reset_future_goals : proofview -> proofview - (** Give an evar the status of a goal (changes its source location - and makes it unresolvable for type classes. *) - val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map + (** Give the evars the status of a goal (changes their source location + and makes them unresolvable for type classes. *) + val mark_as_goals : Evd.evar_map -> Evar.t list -> Evd.evar_map (** Make an evar unresolvable for type classes. *) val mark_as_unresolvable : proofview -> Evar.t -> proofview @@ -475,8 +475,6 @@ module Unsafe : sig val undefined : Evd.evar_map -> Proofview_monad.goal_with_state list -> Proofview_monad.goal_with_state list - val typeclass_resolvable : unit Evd.Store.field - end (** This module gives access to the innards of the monad. Its use is @@ -507,7 +505,6 @@ module Goal : sig val hyps : t -> named_context val env : t -> Environ.env val sigma : t -> Evd.evar_map - val extra : t -> Evd.Store.t val state : t -> Proofview_monad.StateStore.t (** [nf_enter t] applies the goal-dependent tactic [t] in each goal diff --git a/engine/termops.ml b/engine/termops.ml index 1244074d50..5e220fd8f1 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -365,12 +365,18 @@ let pr_evar_map_gen with_univs pr_evars sigma = else str "CONSTRAINTS:" ++ brk (0, 1) ++ pr_evar_constraints sigma conv_pbs ++ fnl () + and typeclasses = + let evars = Evd.get_typeclass_evars sigma in + if Evar.Set.is_empty evars then mt () + else + str "TYPECLASSES:" ++ brk (0, 1) ++ + prlist_with_sep spc Evar.print (Evar.Set.elements evars) ++ fnl () and metas = if List.is_empty (Evd.meta_list sigma) then mt () else str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma in - evs ++ svs ++ cstrs ++ metas + evs ++ svs ++ cstrs ++ typeclasses ++ metas let pr_evar_list sigma l = let open Evd in @@ -816,26 +822,11 @@ let map_constr_with_full_binders_user_view sigma g f = each binder traversal; it is not recursive *) let fold_constr_with_full_binders sigma g f n acc c = - let open RelDecl in - match EConstr.kind sigma c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> acc - | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c - | Lambda (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g (LocalDef (na, b, t)) n) (f n (f n acc b) t) c - | App (c,l) -> Array.fold_left (f n) (f n acc c) l - | Proj (p,c) -> f n acc c - | Evar (_,l) -> Array.fold_left (f n) acc l - | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl - | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd - | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in - let fd = Array.map2 (fun t b -> (t,b)) tl bl in - Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd + let open EConstr in + let f l acc c = f l acc (of_constr c) in + let g d l = g (of_rel_decl d) l in + let c = Unsafe.to_constr (whd_evar sigma c) in + Constr.fold_with_full_binders g f n acc c let fold_constr_with_binders sigma g f n acc c = fold_constr_with_full_binders sigma (fun _ x -> g x) f n acc c @@ -912,9 +903,9 @@ let occur_in_global env id constr = let occur_var env sigma id c = let rec occur_rec c = - match EConstr.kind sigma c with - | Var _ | Const _ | Ind _ | Construct _ -> occur_in_global env id (EConstr.to_constr sigma c) - | _ -> EConstr.iter sigma occur_rec c + match EConstr.destRef sigma c with + | gr, _ -> occur_in_global env id gr + | exception DestKO -> EConstr.iter sigma occur_rec c in try occur_rec c; false with Occur -> true @@ -961,9 +952,7 @@ let collect_vars sigma c = | _ -> EConstr.fold sigma aux vars c in aux Id.Set.empty c -let vars_of_global_reference env gr = - let c, _ = Global.constr_of_global_in_context env gr in - vars_of_global env c +let vars_of_global_reference = vars_of_global (* Tests whether [m] is a subterm of [t]: [m] is appropriately lifted through abstractions of [t] *) @@ -1458,12 +1447,9 @@ let clear_named_body id env = let global_vars_set env sigma constr = let rec filtrec acc c = - let acc = match EConstr.kind sigma c with - | Var _ | Const _ | Ind _ | Construct _ -> - Id.Set.union (vars_of_global env (EConstr.to_constr sigma c)) acc - | _ -> acc - in - EConstr.fold sigma filtrec acc c + match EConstr.destRef sigma c with + | gr, _ -> Id.Set.union (vars_of_global env gr) acc + | exception DestKO -> EConstr.fold sigma filtrec acc c in filtrec Id.Set.empty constr diff --git a/engine/termops.mli b/engine/termops.mli index 64e3977d68..f7b9469ae8 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -118,7 +118,9 @@ val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> bool val count_occurrences : Evd.evar_map -> constr -> constr -> int val collect_metas : Evd.evar_map -> constr -> int list val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *) + val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t +[@@ocaml.deprecated "Use [Environ.vars_of_global]"] (* Substitution of metavariables *) type meta_value_map = (metavariable * Constr.constr) list diff --git a/engine/uState.ml b/engine/uState.ml index 29cb3c9bcc..aa7ec63a6f 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -406,12 +406,25 @@ let check_univ_decl ~poly uctx decl = (Univ.ContextSet.constraints uctx.uctx_local); ctx +let restrict_universe_context (univs, csts) keep = + let open Univ in + let removed = LSet.diff univs keep in + if LSet.is_empty removed then univs, csts + else + let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in + let g = UGraph.empty_universes in + let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in + let g = UGraph.merge_constraints csts g in + let allkept = LSet.diff allunivs removed in + let csts = UGraph.constraints_for ~kept:allkept g in + (LSet.inter univs keep, csts) + let restrict ctx vars = let vars = Univ.LSet.union vars ctx.uctx_seff_univs in let vars = Names.Id.Map.fold (fun na l vars -> Univ.LSet.add l vars) (fst ctx.uctx_names) vars in - let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in + let uctx' = restrict_universe_context ctx.uctx_local vars in { ctx with uctx_local = uctx' } let demote_seff_univs entry uctx = diff --git a/engine/uState.mli b/engine/uState.mli index f833508ebf..8053a7bf83 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -13,6 +13,7 @@ primitives when needed. *) open Names +open Univ exception UniversesDiffer @@ -91,6 +92,16 @@ val universe_of_name : t -> Id.t -> Univ.Level.t (** {5 Unification} *) +(** [restrict_universe_context (univs,csts) keep] restricts [univs] to + the universes in [keep]. The constraints [csts] are adjusted so + that transitive constraints between remaining universes (those in + [keep] and those not in [univs]) are preserved. *) +val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t + +(** [restrict uctx ctx] restricts the local universes of [uctx] to + [ctx] extended by local named universes and side effect universes + (from [demote_seff_univs]). Transitive constraints between retained + universes are preserved. *) val restrict : t -> Univ.LSet.t -> t val demote_seff_univs : Safe_typing.private_constants Entries.definition_entry -> t -> t diff --git a/engine/univGen.ml b/engine/univGen.ml index b07d4848ff..130aa06f53 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -11,7 +11,6 @@ open Sorts open Names open Constr -open Environ open Univ (* Generator of levels *) @@ -32,122 +31,62 @@ 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 = - let init _ = new_univ_level () in - Instance.of_array (Array.init (AUContext.size ctx) init) +let fresh_instance auctx = + let inst = Array.init (AUContext.size auctx) (fun _ -> new_univ_level()) in + let ctx = Array.fold_right LSet.add inst LSet.empty in + let inst = Instance.of_array inst in + inst, (ctx, AUContext.instantiate inst auctx) -let fresh_instance_from_context ctx = - let inst = fresh_universe_instance ctx in - let constraints = AUContext.instantiate inst ctx in - inst, constraints - -let fresh_instance ctx = - let ctx' = ref LSet.empty in - let init _ = - let u = new_univ_level () in - ctx' := LSet.add u !ctx'; u - in - let inst = Instance.of_array (Array.init (AUContext.size ctx) init) - in !ctx', inst - -let existing_instance ctx inst = +let existing_instance ?loc auctx inst = let () = let len1 = Array.length (Instance.to_array inst) - and len2 = AUContext.size ctx in + and len2 = AUContext.size auctx in if not (len1 == len2) then - CErrors.user_err ~hdr:"Universes" - Pp.(str "Polymorphic constant expected " ++ int len2 ++ - str" levels but was given " ++ int len1) + CErrors.user_err ?loc ~hdr:"Universes" + Pp.(str "Universe instance should have length " ++ int len2 ++ str ".") else () - in LSet.empty, inst - -let fresh_instance_from ctx inst = - let ctx', inst = - match inst with - | Some inst -> existing_instance ctx inst - | None -> fresh_instance ctx in - let constraints = AUContext.instantiate inst ctx in - inst, (ctx', constraints) + inst, (LSet.empty, AUContext.instantiate inst auctx) -(** Fresh universe polymorphic construction *) +let fresh_instance_from ?loc ctx = function + | Some inst -> existing_instance ?loc ctx inst + | None -> fresh_instance ctx -let fresh_constant_instance env c inst = - let cb = lookup_constant c env in - match cb.Declarations.const_universes with - | Declarations.Monomorphic_const _ -> ((c,Instance.empty), ContextSet.empty) - | Declarations.Polymorphic_const auctx -> - let inst, ctx = - fresh_instance_from auctx inst - in - ((c, inst), ctx) - -let fresh_inductive_instance env ind inst = - let mib, mip = Inductive.lookup_mind_specif env ind in - match mib.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - ((ind,Instance.empty), ContextSet.empty) - | Declarations.Polymorphic_ind uactx -> - let inst, ctx = (fresh_instance_from uactx) inst in - ((ind,inst), ctx) - | Declarations.Cumulative_ind acumi -> - let inst, ctx = - fresh_instance_from (Univ.ACumulativityInfo.univ_context acumi) inst - in ((ind,inst), ctx) - -let fresh_constructor_instance env (ind,i) inst = - let mib, mip = Inductive.lookup_mind_specif env ind in - match mib.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> (((ind,i),Instance.empty), ContextSet.empty) - | Declarations.Polymorphic_ind auctx -> - let inst, ctx = fresh_instance_from auctx inst in - (((ind,i),inst), ctx) - | Declarations.Cumulative_ind acumi -> - let inst, ctx = fresh_instance_from (ACumulativityInfo.univ_context acumi) inst in - (((ind,i),inst), ctx) +(** Fresh universe polymorphic construction *) open Globnames -let fresh_global_instance ?names env gr = - match gr with - | VarRef id -> mkVar id, ContextSet.empty - | ConstRef sp -> - let c, ctx = fresh_constant_instance env sp names in - mkConstU c, ctx - | ConstructRef sp -> - let c, ctx = fresh_constructor_instance env sp names in - mkConstructU c, ctx - | IndRef sp -> - let c, ctx = fresh_inductive_instance env sp names in - mkIndU c, ctx - -let fresh_constant_instance env sp = - fresh_constant_instance env sp None - -let fresh_inductive_instance env sp = - fresh_inductive_instance env sp None - -let fresh_constructor_instance env sp = - fresh_constructor_instance env sp None - -let constr_of_global gr = - let c, ctx = fresh_global_instance (Global.env ()) gr in - if not (Univ.ContextSet.is_empty ctx) then - if Univ.LSet.is_empty (Univ.ContextSet.levels ctx) then - (* Should be an error as we might forget constraints, allow for now - to make firstorder work with "using" clauses *) - c - else CErrors.user_err ~hdr:"constr_of_global" - Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ - str " would forget universes.") - else 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_instance ?loc ?names env gr = + let auctx = Environ.universes_of_global env gr in + let u, ctx = fresh_instance_from ?loc auctx names in + u, ctx + +let fresh_constant_instance env c = + let u, ctx = fresh_global_instance env (ConstRef c) in + (c, u), ctx + +let fresh_inductive_instance env ind = + let u, ctx = fresh_global_instance env (IndRef ind) in + (ind, u), ctx + +let fresh_constructor_instance env c = + let u, ctx = fresh_global_instance env (ConstructRef c) in + (c, u), ctx + +let fresh_global_instance ?loc ?names env gr = + let u, ctx = fresh_global_instance ?loc ?names env gr in + mkRef (gr, u), ctx + +let constr_of_monomorphic_global gr = + if not (Global.is_polymorphic gr) then + fst (fresh_global_instance (Global.env ()) gr) + else CErrors.user_err ~hdr:"constr_of_global" + Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ + str " would forget universes.") + +let constr_of_global gr = constr_of_monomorphic_global gr + +let constr_of_global_univ = mkRef let fresh_global_or_constr_instance env = function | IsConstr c -> c, ContextSet.empty @@ -166,52 +105,26 @@ 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 let ty = cb.const_type in - begin - match cb.const_universes with - | Monomorphic_const _ -> ty, ContextSet.empty - | Polymorphic_const auctx -> - let inst, ctx = fresh_instance_from auctx None in - Vars.subst_instance_constr inst ty, ctx - end + let auctx = Declareops.constant_polymorphic_context cb in + let inst, ctx = fresh_instance auctx in + Vars.subst_instance_constr inst ty, ctx + | IndRef ind -> - let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in - begin - match mib.mind_universes with - | Monomorphic_ind _ -> - let ty = Inductive.type_of_inductive env (specif, Univ.Instance.empty) in - ty, ContextSet.empty - | Polymorphic_ind auctx -> - let inst, ctx = fresh_instance_from auctx None in - let ty = Inductive.type_of_inductive env (specif, inst) in - ty, ctx - | Cumulative_ind cumi -> - let inst, ctx = - fresh_instance_from (ACumulativityInfo.univ_context cumi) None - in - let ty = Inductive.type_of_inductive env (specif, inst) in - ty, ctx - end - - | ConstructRef cstr -> - let (mib,oib as specif) = - Inductive.lookup_mind_specif env (inductive_of_constructor cstr) - in - begin - match mib.mind_universes with - | Monomorphic_ind _ -> - Inductive.type_of_constructor (cstr,Instance.empty) specif, ContextSet.empty - | Polymorphic_ind auctx -> - let inst, ctx = fresh_instance_from auctx None in - Inductive.type_of_constructor (cstr,inst) specif, ctx - | Cumulative_ind cumi -> - let inst, ctx = - fresh_instance_from (ACumulativityInfo.univ_context cumi) None - in - Inductive.type_of_constructor (cstr,inst) specif, ctx - end + let (mib, _ as specif) = Inductive.lookup_mind_specif env ind in + let auctx = Declareops.inductive_polymorphic_context mib in + let inst, ctx = fresh_instance auctx in + let ty = Inductive.type_of_inductive env (specif, inst) in + ty, ctx + + | ConstructRef (ind,_ as cstr) -> + let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in + let auctx = Declareops.inductive_polymorphic_context mib in + let inst, ctx = fresh_instance auctx in + Inductive.type_of_constructor (cstr,inst) specif, ctx let type_of_global t = type_of_reference (Global.env ()) t @@ -225,8 +138,7 @@ let fresh_sort_in_family = function let new_sort_in_family sf = fst (fresh_sort_in_family sf) -let extend_context (a, ctx) (ctx') = - (a, ContextSet.union ctx ctx') +let extend_context = Univ.extend_in_context_set let new_global_univ () = let u = fresh_level () in diff --git a/engine/univGen.mli b/engine/univGen.mli index 439424934c..8af5f8fdb0 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -23,20 +23,24 @@ val set_remote_new_univ_id : universe_id RemoteCounter.installer val new_univ_id : unit -> universe_id val new_univ_level : unit -> Level.t + val new_univ : unit -> Universe.t +[@@ocaml.deprecated "Use [new_univ_level]"] val new_Type : unit -> types +[@@ocaml.deprecated "Use [new_univ_level]"] val new_Type_sort : unit -> Sorts.t +[@@ocaml.deprecated "Use [new_univ_level]"] val new_global_univ : unit -> Universe.t in_universe_context_set val new_sort_in_family : Sorts.family -> Sorts.t +[@@ocaml.deprecated "Use [fresh_sort_in_family]"] (** Build a fresh instance for a given context, its associated substitution and the instantiated constraints. *) -val fresh_instance_from_context : AUContext.t -> - Instance.t constrained +val fresh_instance : AUContext.t -> Instance.t in_universe_context_set -val fresh_instance_from : AUContext.t -> Instance.t option -> +val fresh_instance_from : ?loc:Loc.t -> AUContext.t -> Instance.t option -> Instance.t in_universe_context_set val fresh_sort_in_family : Sorts.family -> @@ -48,7 +52,7 @@ val fresh_inductive_instance : env -> inductive -> val fresh_constructor_instance : env -> constructor -> pconstructor in_universe_context_set -val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t -> +val fresh_global_instance : ?loc:Loc.t -> ?names:Univ.Instance.t -> env -> GlobRef.t -> constr in_universe_context_set val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> @@ -63,18 +67,26 @@ val fresh_universe_context_set_instance : ContextSet.t -> val global_of_constr : constr -> GlobRef.t puniverses val constr_of_global_univ : GlobRef.t puniverses -> constr +[@@ocaml.deprecated "Use [Constr.mkRef]"] val extend_context : 'a in_universe_context_set -> ContextSet.t -> 'a in_universe_context_set +[@@ocaml.deprecated "Use [Univ.extend_in_context_set]"] (** Create a fresh global in the global environment, without side effects. - BEWARE: this raises an ANOMALY on polymorphic constants/inductives: + BEWARE: this raises an error on polymorphic constants/inductives: the constraints should be properly added to an evd. See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for - the proper way to get a fresh copy of a global reference. *) + the proper way to get a fresh copy of a polymorphic global reference. *) +val constr_of_monomorphic_global : GlobRef.t -> constr + val constr_of_global : GlobRef.t -> constr +[@@ocaml.deprecated "constr_of_global will crash on polymorphic constants,\ + use [constr_of_monomorphic_global] if the reference is guaranteed to\ + be monomorphic, [Evarutil.new_global] or [Tacmach.New.pf_constr_of_global] otherwise"] (** Returns the type of the global reference, by creating a fresh instance of polymorphic references and computing their instantiated universe context. (side-effect on the universe counter, use with care). *) val type_of_global : GlobRef.t -> types in_universe_context_set +[@@ocaml.deprecated "use [Typeops.type_of_global]"] diff --git a/engine/univNames.ml b/engine/univNames.ml index e89dcedb9c..a71f9c5736 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -86,7 +86,7 @@ let register_universe_binders ref ubinders = part of the code that depends on the internal representation of names in abstract contexts, but removing it requires quite a rework of the callers. *) - let univs = AUContext.instance (Global.universes_of_global ref) in + let univs = AUContext.instance (Environ.universes_of_global (Global.env()) ref) in let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in let map lvl = try LMap.find lvl revmap diff --git a/engine/univops.ml b/engine/univops.ml index 7f9672f828..53c42023ad 100644 --- a/engine/univops.ml +++ b/engine/univops.ml @@ -8,30 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Univ -open Constr +let universes_of_constr = Vars.universes_of_constr -let universes_of_constr c = - let rec aux s c = - match kind c with - | Const (c, u) -> - LSet.fold LSet.add (Instance.levels u) s - | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> - LSet.fold LSet.add (Instance.levels u) s - | Sort u when not (Sorts.is_small u) -> - let u = Sorts.univ_of_sort u in - LSet.fold LSet.add (Universe.levels u) s - | _ -> Constr.fold aux s c - in aux LSet.empty c - -let restrict_universe_context (univs, csts) keep = - let removed = LSet.diff univs keep in - if LSet.is_empty removed then univs, csts - else - let allunivs = Constraint.fold (fun (u,_,v) all -> LSet.add u (LSet.add v all)) csts univs in - let g = UGraph.empty_universes in - let g = LSet.fold UGraph.add_universe_unconstrained allunivs g in - let g = UGraph.merge_constraints csts g in - let allkept = LSet.diff allunivs removed in - let csts = UGraph.constraints_for ~kept:allkept g in - (LSet.inter univs keep, csts) +let restrict_universe_context = UState.restrict_universe_context diff --git a/engine/univops.mli b/engine/univops.mli index 57a53597b9..597d2d6785 100644 --- a/engine/univops.mli +++ b/engine/univops.mli @@ -13,9 +13,7 @@ open Univ (** Return the set of all universes appearing in [constr]. *) val universes_of_constr : constr -> LSet.t +[@@ocaml.deprecated "Use [Vars.universes_of_constr]"] -(** [restrict_universe_context (univs,csts) keep] restricts [univs] to - the universes in [keep]. The constraints [csts] are adjusted so - that transitive constraints between remaining universes (those in - [keep] and those not in [univs]) are preserved. *) val restrict_universe_context : ContextSet.t -> LSet.t -> ContextSet.t +[@@ocaml.deprecated "Use [UState.restrict_universe_context]"] |