diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/evarutil.ml | 17 | ||||
| -rw-r--r-- | engine/evarutil.mli | 4 | ||||
| -rw-r--r-- | engine/evd.ml | 14 | ||||
| -rw-r--r-- | engine/evd.mli | 5 | ||||
| -rw-r--r-- | engine/namegen.ml | 14 | ||||
| -rw-r--r-- | engine/proofview.ml | 8 |
6 files changed, 37 insertions, 25 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 339c6a248e..eabfb7b398 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -478,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 = @@ -552,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 @@ -665,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 14173e774d..ee0fae3d46 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -204,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 diff --git a/engine/evd.ml b/engine/evd.ml index f1b5419dec..324f883e8e 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -630,7 +630,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 +642,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 +658,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 +675,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' diff --git a/engine/evd.mli b/engine/evd.mli index abcabe8157..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 *) diff --git a/engine/namegen.ml b/engine/namegen.ml index 1dd29e6eae..2e62b89011 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" 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 = |