diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 7 | ||||
| -rw-r--r-- | engine/evarutil.ml | 27 | ||||
| -rw-r--r-- | engine/evarutil.mli | 13 | ||||
| -rw-r--r-- | engine/evd.ml | 42 | ||||
| -rw-r--r-- | engine/evd.mli | 11 | ||||
| -rw-r--r-- | engine/geninterp.ml | 6 | ||||
| -rw-r--r-- | engine/geninterp.mli | 4 | ||||
| -rw-r--r-- | engine/namegen.ml | 57 | ||||
| -rw-r--r-- | engine/namegen.mli | 26 | ||||
| -rw-r--r-- | engine/proofview.ml | 8 | ||||
| -rw-r--r-- | engine/termops.ml | 64 | ||||
| -rw-r--r-- | engine/termops.mli | 2 | ||||
| -rw-r--r-- | engine/uState.ml | 122 | ||||
| -rw-r--r-- | engine/uState.mli | 26 | ||||
| -rw-r--r-- | engine/universes.ml | 81 | ||||
| -rw-r--r-- | engine/universes.mli | 19 |
16 files changed, 272 insertions, 243 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 7b879a8031..a54c082979 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -566,7 +566,6 @@ let compare_constr sigma cmp c1 c2 = let cmp c1 c2 = cmp (of_constr c1) (of_constr c2) in compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal cmp (unsafe_to_constr c1) (unsafe_to_constr c2) -(** TODO: factorize with universes.ml *) let test_constr_universes sigma leq m n = let open Universes in let kind c = kind_upto sigma c in @@ -574,14 +573,20 @@ let test_constr_universes sigma leq m n = else let cstrs = ref Constraints.empty in let eq_universes strict l l' = + let l = EInstance.kind sigma (EInstance.make l) in + let l' = EInstance.kind sigma (EInstance.make l') in cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in let eq_sorts s1 s2 = + let s1 = ESorts.kind sigma (ESorts.make s1) in + let s2 = ESorts.kind sigma (ESorts.make s2) in if Sorts.equal s1 s2 then true else (cstrs := Constraints.add (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs; true) in let leq_sorts s1 s2 = + let s1 = ESorts.kind sigma (ESorts.make s1) in + let s2 = ESorts.kind sigma (ESorts.make s2) in if Sorts.equal s1 s2 then true else (cstrs := Constraints.add diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 2afc12cd36..38efcca050 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -306,7 +306,7 @@ let push_rel_decl_to_named_context sigma decl (subst, vsubst, avoid, nc) = in let extract_if_neq id = function | Anonymous -> None - | Name id' when id_ord id id' = 0 -> None + | Name id' when Id.compare id id' = 0 -> None | Name id' -> Some id' in let na = RelDecl.get_name decl in @@ -412,6 +412,14 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?prin let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in evd, mkEvar (newevk,Array.of_list instance) +let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?principal 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] 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 env evd ?src ?filter ?candidates ?store ?naming ?principal typ = @@ -470,8 +478,6 @@ type clear_dependency_error = exception ClearDependencyError of Id.t * clear_dependency_error -let cleared = Store.field () - exception Depends of Id.t let rec check_and_clear_in_constr env evdref err ids global c = @@ -544,13 +550,6 @@ let rec check_and_clear_in_constr env evdref err ids global c = let evd = !evdref in let (evd,_) = restrict_evar evd evk filter None in evdref := evd; - (* spiwack: hacking session to mark the old [evk] as having been "cleared" *) - let evi = Evd.find !evdref evk in - let extra = evi.evar_extra in - let extra' = Store.set extra cleared true in - let evi' = { evi with evar_extra = extra' } in - evdref := Evd.add !evdref evk evi' ; - (* spiwack: /hacking session *) Evd.existential_value !evdref ev | _ -> map_constr (check_and_clear_in_constr env evdref err ids global) c @@ -657,11 +656,9 @@ let rec advance sigma evk = match evi.evar_body with | Evar_empty -> Some evk | Evar_defined v -> - if Option.default false (Store.get evi.evar_extra cleared) then - let (evk,_) = Term.destEvar v in - advance sigma evk - else - None + match is_restricted_evar evi with + | Some evk -> advance sigma evk + | None -> None (** The following functions return the set of undefined evars contained in the object, the defined evars being traversed. diff --git a/engine/evarutil.mli b/engine/evarutil.mli index a8b6b5861c..2f85bc7335 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -21,6 +21,13 @@ val new_meta : unit -> metavariable val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) + +val new_evar_from_context : + named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> types -> evar_map * EConstr.t + val new_evar : env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> @@ -197,10 +204,6 @@ type clear_dependency_error = exception ClearDependencyError of Id.t * clear_dependency_error -(* spiwack: marks an evar that has been "defined" by clear. - used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*) -val cleared : bool Store.field - val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types -> Id.Set.t -> named_context_val * types @@ -220,7 +223,7 @@ val push_rel_decl_to_named_context : evar_map -> rel_declaration -> ext_named_context -> ext_named_context val push_rel_context_to_named_context : Environ.env -> evar_map -> types -> - named_context_val * types * constr list * csubst * (identifier*constr) list + named_context_val * types * constr list * csubst * (Id.t*constr) list val generalize_evar_over_rels : evar_map -> existential -> types * constr list diff --git a/engine/evd.ml b/engine/evd.ml index cfc9aa6351..86ab2263f5 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -124,8 +124,7 @@ end (* The type of mappings for existential variables *) -module Dummy = struct end -module Store = Store.Make(Dummy) +module Store = Store.Make () type evar = Term.existential_key @@ -371,17 +370,17 @@ val key : Id.t -> t -> Evar.t end = struct -type t = Id.t EvMap.t * existential_key Idmap.t +type t = Id.t EvMap.t * existential_key Id.Map.t -let empty = (EvMap.empty, Idmap.empty) +let empty = (EvMap.empty, Id.Map.empty) let add_name_newly_undefined id evk evi (evtoid, idtoev as names) = match id with | None -> names | Some id -> - if Idmap.mem id idtoev then + if Id.Map.mem id idtoev then user_err (str "Already an existential evar of name " ++ pr_id id); - (EvMap.add evk id evtoid, Idmap.add id evk idtoev) + (EvMap.add evk id evtoid, Id.Map.add id evk idtoev) let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) = if EvMap.mem evk evtoid then @@ -393,15 +392,15 @@ let remove_name_defined evk (evtoid, idtoev as names) = let id = try Some (EvMap.find evk evtoid) with Not_found -> None in match id with | None -> names - | Some id -> (EvMap.remove evk evtoid, Idmap.remove id idtoev) + | Some id -> (EvMap.remove evk evtoid, Id.Map.remove id idtoev) let rename evk id (evtoid, idtoev) = let id' = try Some (EvMap.find evk evtoid) with Not_found -> None in match id' with - | None -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev) + | None -> (EvMap.add evk id evtoid, Id.Map.add id evk idtoev) | Some id' -> - if Idmap.mem id idtoev then anomaly (str "Evar name already in use."); - (EvMap.update evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev)) + if Id.Map.mem id idtoev then anomaly (str "Evar name already in use."); + (EvMap.update evk id evtoid (* overwrite old name *), Id.Map.add id evk (Id.Map.remove id' idtoev)) let reassign_name_defined evk evk' (evtoid, idtoev as names) = let id = try Some (EvMap.find evk evtoid) with Not_found -> None in @@ -409,13 +408,13 @@ let reassign_name_defined evk evk' (evtoid, idtoev as names) = | None -> names (** evk' must not be defined *) | Some id -> (EvMap.add evk' id (EvMap.remove evk evtoid), - Idmap.add id evk' (Idmap.remove id idtoev)) + Id.Map.add id evk' (Id.Map.remove id idtoev)) let ident evk (evtoid, _) = try Some (EvMap.find evk evtoid) with Not_found -> None let key id (_, idtoev) = - Idmap.find id idtoev + Id.Map.find id idtoev end @@ -630,7 +629,9 @@ 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 define_aux def undef evk body = +let restricted = Store.field () + +let define_aux ?dorestrict def undef evk body = let oldinfo = try EvMap.find evk undef with Not_found -> @@ -640,7 +641,10 @@ let define_aux def undef evk body = anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.") in let () = assert (oldinfo.evar_body == Evar_empty) in - let newinfo = { oldinfo with evar_body = Evar_defined body } 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 EvMap.add evk newinfo def, EvMap.remove evk undef (* define the existential of section path sp as the constr body *) @@ -653,6 +657,9 @@ let define evk body evd = let evar_names = EvNames.remove_name_defined evk evd.evar_names in { evd with defn_evars; undf_evars; last_mods; evar_names } +let is_restricted_evar evi = + Store.get evi.evar_extra restricted + let restrict evk filter ?candidates ?src evd = let evk' = new_untyped_evar () in let evar_info = EvMap.find evk evd.undf_evars in @@ -667,7 +674,7 @@ 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 evd.defn_evars evd.undf_evars evk body in + let (defn_evars, undf_evars) = define_aux ~dorestrict:evk' evd.defn_evars evd.undf_evars evk body in { evd with undf_evars = EvMap.add evk' evar_info' undf_evars; defn_evars; last_mods; evar_names }, evk' @@ -748,7 +755,10 @@ let evar_universe_context d = d.universes let universe_context_set d = UState.context_set d.universes -let universe_context ?names evd = UState.universe_context ?names evd.universes +let universe_context ~names ~extensible evd = + UState.universe_context ~names ~extensible evd.universes + +let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl let restrict_universe_context evd vars = { evd with universes = UState.restrict evd.universes vars } diff --git a/engine/evd.mli b/engine/evd.mli index 3f00a3b0b2..96e4b6acce 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -31,7 +31,7 @@ open Environ (** {6 Evars} *) type evar = existential_key -(** Existential variables. TODO: Should be made opaque one day. *) +(** Existential variables. *) val string_of_existential : evar -> string @@ -244,6 +244,9 @@ val restrict : evar -> Filter.t -> ?candidates:constr list -> (** Restrict an undefined evar into a new evar by filtering context and possibly limiting the instances to a set of candidates *) +val is_restricted_evar : evar_info -> evar option +(** Tell if an evar comes from restriction of another evar, and if yes, which *) + val downcast : evar -> types -> 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 *) @@ -493,7 +496,7 @@ val empty_evar_universe_context : evar_universe_context val union_evar_universe_context : evar_universe_context -> evar_universe_context -> evar_universe_context val evar_universe_context_subst : evar_universe_context -> Universes.universe_opt_subst -val constrain_variables : Univ.LSet.t -> evar_universe_context -> Univ.constraints +val constrain_variables : Univ.LSet.t -> evar_universe_context -> evar_universe_context val evar_universe_context_of_binders : @@ -547,11 +550,13 @@ val check_leq : evar_map -> Univ.universe -> Univ.universe -> bool val evar_universe_context : evar_map -> evar_universe_context val universe_context_set : evar_map -> Univ.universe_context_set -val universe_context : ?names:(Id.t located) list -> evar_map -> +val universe_context : names:(Id.t located) list -> extensible:bool -> evar_map -> (Id.t * Univ.Level.t) list * Univ.universe_context val universe_subst : evar_map -> Universes.universe_opt_subst val universes : evar_map -> UGraph.t +val check_univ_decl : evar_map -> UState.universe_decl -> + Universes.universe_binders * Univ.universe_context val merge_universe_context : evar_map -> evar_universe_context -> evar_map val set_universe_context : evar_map -> evar_universe_context -> evar_map diff --git a/engine/geninterp.ml b/engine/geninterp.ml index e79e258fbc..768ef3cfd9 100644 --- a/engine/geninterp.ml +++ b/engine/geninterp.ml @@ -9,11 +9,11 @@ open Names open Genarg -module TacStore = Store.Make(struct end) +module TacStore = Store.Make () (** Dynamic toplevel values *) -module ValT = Dyn.Make(struct end) +module ValT = Dyn.Make () module Val = struct @@ -47,6 +47,8 @@ struct end +module ValTMap = ValT.Map + module ValReprObj = struct type ('raw, 'glb, 'top) obj = 'top Val.tag diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 492e372adb..ae0b26e594 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -39,6 +39,10 @@ sig val inject : 'a tag -> 'a -> t end + +module ValTMap (M : Dyn.TParam) : + Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ + (** Dynamic types for toplevel values. While the generic types permit to relate objects at various levels of interpretation, toplevel values are wearing their own type regardless of where they came from. This allows to use the diff --git a/engine/namegen.ml b/engine/namegen.ml index a75fe721f7..c548fc4ac9 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -43,6 +43,8 @@ let default_non_dependent_ident = Id.of_string default_non_dependent_string let default_dependent_ident = Id.of_string "x" +let default_generated_non_letter_string = "x" + (**********************************************************************) (* Globality of identifiers *) @@ -107,7 +109,17 @@ let head_name sigma c = (* Find the head constant of a constr if any *) hdrec c let lowercase_first_char id = (* First character of a constr *) - Unicode.lowercase_first_char (Id.to_string id) + let s = Id.to_string id in + match Unicode.split_at_first_letter s with + | None -> + (* General case: nat -> n *) + Unicode.lowercase_first_char s + | Some (s,s') -> + if String.length s' = 0 then + (* No letter, e.g. __, or __'_, etc. *) + default_generated_non_letter_string + else + s ^ Unicode.lowercase_first_char s' let sort_hdchar = function | Prop(_) -> "P" @@ -120,8 +132,8 @@ let hdchar env sigma c = | Cast (c,_,_) | App (c,_) -> hdrec k c | Proj (kn,_) -> lowercase_first_char (Label.to_id (con_label (Projection.constant kn))) | Const (kn,_) -> lowercase_first_char (Label.to_id (con_label kn)) - | Ind (x,_) -> lowercase_first_char (basename_of_global (IndRef x)) - | Construct (x,_) -> lowercase_first_char (basename_of_global (ConstructRef x)) + | 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") | Var id -> lowercase_first_char id | Sort s -> sort_hdchar (ESorts.kind sigma s) | Rel n -> @@ -239,7 +251,7 @@ let visible_ids sigma (nenv, c) = let next_name_away_in_cases_pattern sigma env_t na avoid = let id = match na with Name id -> id | Anonymous -> default_dependent_ident in let visible = visible_ids sigma env_t in - let bad id = Id.List.mem id avoid || is_constructor id + let bad id = Id.Set.mem id avoid || is_constructor id || Id.Set.mem id visible in next_ident_away_from id bad @@ -253,8 +265,8 @@ let next_name_away_in_cases_pattern sigma env_t na avoid = name is taken by finding a free subscript starting from 0 *) let next_ident_away_in_goal id avoid = - let id = if Id.List.mem id avoid then restart_subscript id else id in - let bad id = Id.List.mem id avoid || (is_global id && not (is_section_variable id)) in + let id = if Id.Set.mem id avoid then restart_subscript id else id in + let bad id = Id.Set.mem id avoid || (is_global id && not (is_section_variable id)) in next_ident_away_from id bad let next_name_away_in_goal na avoid = @@ -271,16 +283,16 @@ let next_name_away_in_goal na avoid = beyond the current subscript *) let next_global_ident_away id avoid = - let id = if Id.List.mem id avoid then restart_subscript id else id in - let bad id = Id.List.mem id avoid || is_global id in + let id = if Id.Set.mem id avoid then restart_subscript id else id in + let bad id = Id.Set.mem id avoid || is_global id in next_ident_away_from id bad (* 4- Looks for next fresh name outside a list; if name already used, looks for same name with lower available subscript *) let next_ident_away id avoid = - if Id.List.mem id avoid then - next_ident_away_from (restart_subscript id) (fun id -> Id.List.mem id avoid) + if Id.Set.mem id avoid then + next_ident_away_from (restart_subscript id) (fun id -> Id.Set.mem id avoid) else id let next_name_away_with_default default na avoid = @@ -302,7 +314,7 @@ let next_name_away = next_name_away_with_default default_non_dependent_string let make_all_name_different env sigma = (** FIXME: this is inefficient, but only used in printing *) - let avoid = ref (Id.Set.elements (Context.Named.to_vars (named_context env))) in + let avoid = ref (ids_of_named_context_val (named_context_val env)) in let sign = named_context_val env in let rels = rel_context env in let env0 = reset_with_named_context sign env in @@ -310,7 +322,7 @@ let make_all_name_different env sigma = (fun decl newenv -> let na = named_hd newenv sigma (RelDecl.get_type decl) (RelDecl.get_name decl) in let id = next_name_away na !avoid in - avoid := id::!avoid; + avoid := Id.Set.add id !avoid; push_rel (RelDecl.set_name (Name id) decl) newenv) rels ~init:env0 @@ -321,7 +333,7 @@ let make_all_name_different env sigma = let next_ident_away_for_default_printing sigma env_t id avoid = let visible = visible_ids sigma env_t in - let bad id = Id.List.mem id avoid || Id.Set.mem id visible in + let bad id = Id.Set.mem id avoid || Id.Set.mem id visible in next_ident_away_from id bad let next_name_away_for_default_printing sigma env_t na avoid = @@ -364,14 +376,21 @@ let next_name_for_display sigma flags = | RenamingElsewhereFor env_t -> next_name_away_for_default_printing sigma env_t (* Remark: Anonymous var may be dependent in Evar's contexts *) -let compute_displayed_name_in sigma flags avoid na c = +let compute_displayed_name_in_gen_poly noccurn_fun sigma flags avoid na c = match na with - | Anonymous when noccurn sigma 1 c -> + | Anonymous when noccurn_fun sigma 1 c -> (Anonymous,avoid) | _ -> let fresh_id = next_name_for_display sigma flags na avoid in - let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in - (idopt, fresh_id::avoid) + let idopt = if noccurn_fun sigma 1 c then Anonymous else Name fresh_id in + (idopt, Id.Set.add fresh_id avoid) + +let compute_displayed_name_in = compute_displayed_name_in_gen_poly noccurn + +let compute_displayed_name_in_gen f sigma = + (* only flag which does not need a constr, maybe to be refined *) + let flag = RenamingForGoal in + compute_displayed_name_in_gen_poly f sigma flag let compute_and_force_displayed_name_in sigma flags avoid na c = match na with @@ -379,11 +398,11 @@ let compute_and_force_displayed_name_in sigma flags avoid na c = (Anonymous,avoid) | _ -> let fresh_id = next_name_for_display sigma flags na avoid in - (Name fresh_id, fresh_id::avoid) + (Name fresh_id, Id.Set.add fresh_id avoid) let compute_displayed_let_name_in sigma flags avoid na c = let fresh_id = next_name_for_display sigma flags na avoid in - (Name fresh_id, fresh_id::avoid) + (Name fresh_id, Id.Set.add fresh_id avoid) let rename_bound_vars_as_displayed sigma avoid env c = let rec rename avoid env c = diff --git a/engine/namegen.mli b/engine/namegen.mli index 14846a9184..d29b69259f 100644 --- a/engine/namegen.mli +++ b/engine/namegen.mli @@ -72,23 +72,22 @@ val next_ident_away_from : Id.t -> (Id.t -> bool) -> Id.t the whole identifier except for the {i subscript}. E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *) -val next_ident_away : Id.t -> Id.t list -> Id.t +val next_ident_away : Id.t -> Id.Set.t -> Id.t (** Avoid clashing with a name already used in current module *) -val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t +val next_ident_away_in_goal : Id.t -> Id.Set.t -> Id.t (** Avoid clashing with a name already used in current module but tolerate overwriting section variables, as in goals *) -val next_global_ident_away : Id.t -> Id.t list -> Id.t +val next_global_ident_away : Id.t -> Id.Set.t -> Id.t (** Default is [default_non_dependent_ident] *) -val next_name_away : Name.t -> Id.t list -> Id.t +val next_name_away : Name.t -> Id.Set.t -> Id.t -val next_name_away_with_default : string -> Name.t -> Id.t list -> - Id.t +val next_name_away_with_default : string -> Name.t -> Id.Set.t -> Id.t val next_name_away_with_default_using_types : string -> Name.t -> - Id.t list -> types -> Id.t + Id.Set.t -> types -> Id.t val set_reserved_typed_name : (types -> Name.t) -> unit @@ -103,13 +102,18 @@ type renaming_flags = val make_all_name_different : env -> evar_map -> env val compute_displayed_name_in : - evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list + evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t val compute_and_force_displayed_name_in : - evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list + evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t val compute_displayed_let_name_in : - evar_map -> renaming_flags -> Id.t list -> Name.t -> constr -> Name.t * Id.t list + evar_map -> renaming_flags -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t val rename_bound_vars_as_displayed : - evar_map -> Id.t list -> Name.t list -> types -> types + evar_map -> Id.Set.t -> Name.t list -> types -> types + +(* Generic function expecting a "not occurn" function *) +val compute_displayed_name_in_gen : + (evar_map -> int -> 'a -> bool) -> + evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t (**********************************************************************) (* Naming strategy for arguments in Prop when eliminating inductive types *) diff --git a/engine/proofview.ml b/engine/proofview.ml index eef2b83f44..598358c472 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -153,8 +153,12 @@ let focus i j sp = ( { sp with comb = new_comb } , context ) (** [undefined defs l] is the list of goals in [l] which are still - unsolved (after advancing cleared goals). *) -let undefined defs l = CList.map_filter (Evarutil.advance defs) l + unsolved (after advancing cleared goals). Note that order matters. *) +let undefined defs l = + List.fold_right (fun evk l -> + match Evarutil.advance defs evk with + | Some evk -> List.add_set Evar.equal evk l + | None -> l) l [] (** Unfocuses a proofview with respect to a context. *) let unfocus c sp = diff --git a/engine/termops.ml b/engine/termops.ml index 2bd0c06d6d..76f707f945 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -327,11 +327,11 @@ let pr_evar_constraints sigma pbs = Namegen.make_all_name_different env sigma in print_env_short env ++ spc () ++ str "|-" ++ spc () ++ - print_constr_env env sigma (EConstr.of_constr t1) ++ spc () ++ + protect (print_constr_env env sigma) (EConstr.of_constr t1) ++ spc () ++ str (match pbty with | Reduction.CONV -> "==" | Reduction.CUMUL -> "<=") ++ - spc () ++ print_constr_env env Evd.empty (EConstr.of_constr t2) + spc () ++ protect (print_constr_env env Evd.empty) (EConstr.of_constr t2) in prlist_with_sep fnl pr_evconstr pbs @@ -358,37 +358,37 @@ let pr_evar_list sigma l = h 0 (str (string_of_existential ev) ++ str "==" ++ pr_evar_info evi ++ (if evi.evar_body == Evar_empty - then str " {" ++ pr_existential_key sigma ev ++ str "}" + then str " {" ++ pr_existential_key sigma ev ++ str "}" else mt ())) in h 0 (prlist_with_sep fnl pr l) -let pr_evar_by_depth depth sigma = match depth with -| None -> - (* Print all evars *) - let to_list d = - let open Evd in - (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *) - let l = ref [] in - let fold_def evk evi () = match evi.evar_body with +let to_list d = + let open Evd in + (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *) + let l = ref [] in + let fold_def evk evi () = match evi.evar_body with | Evar_defined _ -> l := (evk, evi) :: !l | Evar_empty -> () - in - let fold_undef evk evi () = match evi.evar_body with + in + let fold_undef evk evi () = match evi.evar_body with | Evar_empty -> l := (evk, evi) :: !l | Evar_defined _ -> () - in - Evd.fold fold_def d (); - Evd.fold fold_undef d (); - !l in - str"EVARS:"++brk(0,1)++pr_evar_list sigma (to_list sigma)++fnl() -| Some n -> + Evd.fold fold_def d (); + Evd.fold fold_undef d (); + !l + +let pr_evar_by_depth depth sigma = match depth with +| None -> (* Print all evars *) + str"EVARS:" ++ brk(0,1) ++ pr_evar_list sigma (to_list sigma) ++ fnl() +| Some n -> + (* Print closure of undefined evars *) str"UNDEFINED EVARS:"++ (if Int.equal n 0 then mt() else str" (+level "++int n++str" closure):")++ brk(0,1)++ - pr_evar_list sigma (evar_dependency_closure n sigma)++fnl() + pr_evar_list sigma (evar_dependency_closure n sigma) ++ fnl() let pr_evar_by_filter filter sigma = let open Evd in @@ -1071,9 +1071,9 @@ let replace_term_gen sigma eq_fun c by_c in_t = let replace_term sigma c byc t = replace_term_gen sigma EConstr.eq_constr c byc t let vars_of_env env = - let s = - Context.Named.fold_outside (fun decl s -> Id.Set.add (NamedDecl.get_id decl) s) - (named_context env) ~init:Id.Set.empty in + let s = Environ.ids_of_named_context_val (Environ.named_context_val env) in + if List.is_empty (Environ.rel_context env) then s + else Context.Rel.fold_outside (fun decl s -> match RelDecl.get_name decl with Name id -> Id.Set.add id s | _ -> s) (rel_context env) ~init:s @@ -1165,6 +1165,24 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with | Cast (c,_,_) -> is_Prop sigma c | _ -> false +let rec is_Set sigma c = match EConstr.kind sigma c with + | Sort u -> + begin match EConstr.ESorts.kind sigma u with + | Prop Pos -> true + | _ -> false + end + | Cast (c,_,_) -> is_Set sigma c + | _ -> false + +let rec is_Type sigma c = match EConstr.kind sigma c with + | Sort u -> + begin match EConstr.ESorts.kind sigma u with + | Type _ -> true + | _ -> false + end + | Cast (c,_,_) -> is_Type sigma c + | _ -> false + (* eq_constr extended with universe erasure *) let compare_constr_univ sigma f cv_pb t1 t2 = let open EConstr in diff --git a/engine/termops.mli b/engine/termops.mli index 2624afd30d..ef2c52a455 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -267,6 +267,8 @@ val isGlobalRef : Evd.evar_map -> constr -> bool val is_template_polymorphic : env -> Evd.evar_map -> constr -> bool val is_Prop : Evd.evar_map -> constr -> bool +val is_Set : Evd.evar_map -> constr -> bool +val is_Type : Evd.evar_map -> constr -> bool (** Combinators on judgments *) diff --git a/engine/uState.ml b/engine/uState.ml index 63bd247d56..13a9bb3732 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -97,17 +97,9 @@ let subst ctx = ctx.uctx_univ_variables let ugraph ctx = ctx.uctx_universes -let algebraics ctx = ctx.uctx_univ_algebraic +let initial_graph ctx = ctx.uctx_initial_universes -let constrain_variables diff ctx = - Univ.LSet.fold - (fun l cstrs -> - try - match Univ.LMap.find l ctx.uctx_univ_variables with - | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs - | None -> cstrs - with Not_found | Option.IsNone -> cstrs) - diff Univ.Constraint.empty +let algebraics ctx = ctx.uctx_univ_algebraic let add_uctx_names ?loc s l (names, names_rev) = (UNameMap.add s l names, Univ.LMap.add l { uname = Some s; uloc = loc } names_rev) @@ -240,6 +232,24 @@ let add_universe_constraints ctx cstrs = uctx_univ_variables = vars; uctx_universes = UGraph.merge_constraints local' ctx.uctx_universes } +let constrain_variables diff ctx = + let univs, local = ctx.uctx_local in + let univs, vars, local = + Univ.LSet.fold + (fun l (univs, vars, cstrs) -> + try + match Univ.LMap.find l vars with + | Some u -> + (Univ.LSet.add l univs, + Univ.LMap.remove l vars, + Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs) + | None -> (univs, vars, cstrs) + with Not_found | Option.IsNone -> (univs, vars, cstrs)) + diff (univs, ctx.uctx_univ_variables, local) + in + { ctx with uctx_local = (univs, local); uctx_univ_variables = vars } + + let pr_uctx_level uctx = let map, map_rev = uctx.uctx_names in fun l -> @@ -247,41 +257,63 @@ let pr_uctx_level uctx = with Not_found | Option.IsNone -> Universes.pr_with_global_universes l -let universe_context ?names ctx = - match names with - | None -> [], Univ.ContextSet.to_context ctx.uctx_local - | Some pl -> - let levels = Univ.ContextSet.levels ctx.uctx_local in - let newinst, map, left = - List.fold_right - (fun (loc,id) (newinst, map, acc) -> - let l = - try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) - with Not_found -> - user_err ?loc ~hdr:"universe_context" - (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") - in (l :: newinst, (id, l) :: map, Univ.LSet.remove l acc)) - pl ([], [], levels) - in - if not (Univ.LSet.is_empty left) then - let n = Univ.LSet.cardinal left in - let loc = - try - let info = - Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in - info.uloc - with Not_found -> None - in - user_err ?loc ~hdr:"universe_context" - ((str(CString.plural n "Universe") ++ spc () ++ - Univ.LSet.pr (pr_uctx_level ctx) left ++ - spc () ++ str (CString.conjugate_verb_to_be n) ++ - str" unbound.")) - else - let inst = Univ.Instance.of_array (Array.of_list newinst) in - let ctx = Univ.UContext.make (inst, - Univ.ContextSet.constraints ctx.uctx_local) - in map, ctx +type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + +let universe_context ~names ~extensible ctx = + let levels = Univ.ContextSet.levels ctx.uctx_local in + let newinst, left = + List.fold_right + (fun (loc,id) (newinst, acc) -> + let l = + try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) + with Not_found -> + user_err ?loc ~hdr:"universe_context" + (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") + in (l :: newinst, Univ.LSet.remove l acc)) + names ([], levels) + in + if not extensible && not (Univ.LSet.is_empty left) then + let n = Univ.LSet.cardinal left in + let loc = + try + let info = + Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in + info.uloc + with Not_found -> None + in + user_err ?loc ~hdr:"universe_context" + ((str(CString.plural n "Universe") ++ spc () ++ + Univ.LSet.pr (pr_uctx_level ctx) left ++ + spc () ++ str (CString.conjugate_verb_to_be n) ++ + str" unbound.")) + else + let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in + let inst = Array.append (Array.of_list newinst) left in + let inst = Univ.Instance.of_array inst in + let map = List.map (fun (s,l) -> Id.of_string s, l) (UNameMap.bindings (fst ctx.uctx_names)) in + let ctx = Univ.UContext.make (inst, + Univ.ContextSet.constraints ctx.uctx_local) in + map, ctx + +let check_implication uctx cstrs ctx = + let gr = initial_graph uctx in + let grext = UGraph.merge_constraints cstrs gr in + let cstrs' = Univ.UContext.constraints ctx in + if UGraph.check_constraints cstrs' grext then () + else CErrors.user_err ~hdr:"check_univ_decl" + (str "Universe constraints are not implied by the ones declared.") + +let check_univ_decl uctx decl = + let open Misctypes in + let pl, ctx = universe_context + ~names:decl.univdecl_instance + ~extensible:decl.univdecl_extensible_instance + uctx + in + if not decl.univdecl_extensible_constraints then + check_implication uctx decl.univdecl_constraints ctx; + pl, ctx let restrict ctx vars = let uctx' = Univops.restrict_universe_context ctx.uctx_local vars in diff --git a/engine/uState.mli b/engine/uState.mli index d198fbfbe9..c44f2c1d74 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -44,6 +44,9 @@ val subst : t -> Universes.universe_opt_subst val ugraph : t -> UGraph.t (** The current graph extended with the local constraints *) +val initial_graph : t -> UGraph.t +(** The initial graph with just the declarations of new universes. *) + val algebraics : t -> Univ.LSet.t (** The subset of unification variables that can be instantiated with algebraic universes as they appear in inferred types only. *) @@ -105,7 +108,7 @@ val is_sort_variable : t -> Sorts.t -> Univ.Level.t option val normalize_variables : t -> Univ.universe_subst * t -val constrain_variables : Univ.LSet.t -> t -> Univ.constraints +val constrain_variables : Univ.LSet.t -> t -> t val abstract_undefined_variables : t -> t @@ -115,9 +118,26 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst val normalize : t -> t -(** {5 TODO: Document me} *) +(** [universe_context names extensible ctx] + + Return a universe context containing the local universes of [ctx] + and their constraints. The universes corresponding to [names] come + first in the order defined by that list. + + If [extensible] is false, check that the universes of [names] are + the only local universes. -val universe_context : ?names:(Id.t Loc.located) list -> t -> (Id.t * Univ.Level.t) list * Univ.universe_context + Also return the association list of universe names and universes + (including those not in [names]). *) +val universe_context : names:(Id.t Loc.located) list -> extensible:bool -> t -> + (Id.t * Univ.Level.t) list * Univ.universe_context + +type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + +val check_univ_decl : t -> universe_decl -> Universes.universe_binders * Univ.universe_context + +(** {5 TODO: Document me} *) val update_sigma_env : t -> Environ.env -> t diff --git a/engine/universes.ml b/engine/universes.ml index 719af43edf..7f5bf24b74 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -14,7 +14,7 @@ open Environ open Univ open Globnames -let pr_with_global_universes l = +let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ()))) with Not_found -> Level.pr l @@ -31,7 +31,7 @@ let universe_binders_of_global ref = let register_universe_binders ref l = universe_binders_table := Refmap.add ref l !universe_binders_table - + (* To disallow minimization to Set *) let set_minimization = ref true @@ -131,47 +131,6 @@ let to_constraints g s = "to_constraints: non-trivial algebraic constraint between universes") in Constraints.fold tr s Constraint.empty -let test_constr_univs_infer leq univs fold m n accu = - if m == n then Some accu - else - let cstrs = ref accu in - let eq_universes strict l l' = UGraph.check_eq_instances univs l l' in - let eq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - match fold (Constraints.singleton (u1, UEq, u2)) !cstrs with - | None -> false - | Some accu -> cstrs := accu; true - in - let leq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in - match fold (Constraints.singleton (u1, ULe, u2)) !cstrs with - | None -> false - | Some accu -> cstrs := accu; true - in - let rec eq_constr' m n = - m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n - in - let res = - if leq then - let rec compare_leq m n = - Constr.compare_head_gen_leq eq_universes leq_sorts - eq_constr' leq_constr' m n - and leq_constr' m n = m == n || compare_leq m n in - compare_leq m n - else Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n - in - if res then Some !cstrs else None - -let eq_constr_univs_infer univs fold m n accu = - test_constr_univs_infer false univs fold m n accu - -let leq_constr_univs_infer univs fold m n accu = - test_constr_univs_infer true univs fold m n accu - (** Variant of [eq_constr_univs_infer] taking kind-of-term functions, to expose subterms of [m] and [n], arguments. *) let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = @@ -197,42 +156,6 @@ let eq_constr_univs_infer_with kind1 kind2 univs fold m n accu = let res = Constr.compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq_constr' m n in if res then Some !cstrs else None -let test_constr_universes leq m n = - if m == n then Some Constraints.empty - else - let cstrs = ref Constraints.empty in - let eq_universes strict l l' = - cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in - let eq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else (cstrs := Constraints.add - (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs; - true) - in - let leq_sorts s1 s2 = - if Sorts.equal s1 s2 then true - else - (cstrs := Constraints.add - (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs; - true) - in - let rec eq_constr' m n = - m == n || Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n - in - let res = - if leq then - let rec compare_leq m n = - Constr.compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n - and leq_constr' m n = m == n || compare_leq m n in - compare_leq m n - else - Constr.compare_head_gen eq_universes eq_sorts eq_constr' m n - in - if res then Some !cstrs else None - -let eq_constr_universes m n = test_constr_universes false m n -let leq_constr_universes m n = test_constr_universes true m n - let compare_head_gen_proj env equ eqs eqc' m n = match kind_of_term m, kind_of_term n with | Proj (p, c), App (f, args) diff --git a/engine/universes.mli b/engine/universes.mli index fe40f82385..8b2217d446 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -67,11 +67,6 @@ val enforce_eq_instances_univs : bool -> universe_instance universe_constraint_f val to_constraints : UGraph.t -> universe_constraints -> constraints -(** [eq_constr_univs_infer u a b] is [true, c] if [a] equals [b] modulo alpha, casts, - application grouping, the universe constraints in [u] and additional constraints [c]. *) -val eq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> - constr -> constr -> 'a -> 'a option - (** [eq_constr_univs_infer_With kind1 kind2 univs m n] is a variant of {!eq_constr_univs_infer} taking kind-of-term functions, to expose subterms of [m] and [n], arguments. *) @@ -80,20 +75,6 @@ val eq_constr_univs_infer_with : (constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term) -> UGraph.t -> 'a constraint_accumulator -> constr -> constr -> 'a -> 'a option -(** [leq_constr_univs u a b] is [true, c] if [a] is convertible to [b] - modulo alpha, casts, application grouping, the universe constraints - in [u] and additional constraints [c]. *) -val leq_constr_univs_infer : UGraph.t -> 'a constraint_accumulator -> - constr -> constr -> 'a -> 'a option - -(** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, - application grouping and the universe constraints in [c]. *) -val eq_constr_universes : constr -> constr -> universe_constraints option - -(** [leq_constr_universes a b] [true, c] if [a] is convertible to [b] modulo - alpha, casts, application grouping and the universe constraints in [c]. *) -val leq_constr_universes : constr -> constr -> universe_constraints option - (** [eq_constr_universes a b] [true, c] if [a] equals [b] modulo alpha, casts, application grouping and the universe constraints in [c]. *) val eq_constr_universes_proj : env -> constr -> constr -> bool universe_constrained |