From 538b77dbb3b7799dc4d2e18033fc4fbf2eb26f7f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 30 Sep 2014 09:13:40 +0200 Subject: Add syntax for naming new goals in refine: writing ?[id] instead of _ will name the goal id; writing ?[?id] will use the first fresh name available based with prefix id. Tactics intro, rename, change, ... from logic.ml now preserve goal name; cut preserves goal name on its main premise. --- pretyping/cases.ml | 2 +- pretyping/detyping.ml | 4 ++-- pretyping/evarutil.ml | 24 ++++++++++++------------ pretyping/evarutil.mli | 18 ++++++++++++------ pretyping/evd.ml | 43 ++++++++++++++++++++++++++++++++----------- pretyping/evd.mli | 6 ++++-- pretyping/glob_ops.ml | 9 +++++---- pretyping/miscops.ml | 7 +++++++ pretyping/miscops.mli | 5 +++++ pretyping/patternops.ml | 2 +- pretyping/pretyping.ml | 10 +++++----- 11 files changed, 86 insertions(+), 44 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c9c6cecb1..d52830a16 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1946,7 +1946,7 @@ let mk_JMeq evdref typ x typ' y = let mk_JMeq_refl evdref typ x = papp evdref coq_JMeq_refl [| typ; x |] -let hole = GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define true), None) +let hole = GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define true), Misctypes.IntroAnonymous, None) let constr_of_pat env evdref arsign pat avoid = let rec typ env (ty, realargs) pat avoid = diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 0b0ff2fb5..df3d243f1 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -737,7 +737,7 @@ let rec subst_glob_constr subst raw = | GSort _ -> raw - | GHole (loc, knd, solve) -> + | GHole (loc, knd, naming, solve) -> let nknd = match knd with | Evar_kinds.ImplicitArg (ref, i, b) -> let nref, _ = subst_global subst ref in @@ -746,7 +746,7 @@ let rec subst_glob_constr subst raw = in let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in if nsolve == solve && nknd == knd then raw - else GHole (loc, nknd, nsolve) + else GHole (loc, nknd, naming, nsolve) | GCast (loc,r1,k) -> let r1' = subst_glob_constr subst r1 in diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 64bdb90a2..cebb45266 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -358,35 +358,35 @@ let new_pure_evar_full evd evi = let evd = Evd.add evd evk evi in (evd, evk) -let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store typ = +let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) typ = let newevk = new_untyped_evar() in - let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store evd in + let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store ~naming evd in (evd,newevk) -let new_evar_instance sign evd typ ?src ?filter ?candidates ?store instance = +let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) instance = 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 typ in + let evd,newevk = new_pure_evar sign evd ?src ?filter ?candidates ?store ~naming typ in (evd,mkEvar (newevk,Array.of_list 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 typ = +let new_evar env evd ?src ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) typ = let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in let candidates = Option.map (List.map (subst2 subst vsubst)) candidates 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 instance + new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ~naming instance -let new_type_evar env evd ?src ?filter rigid = +let new_type_evar env evd ?src ?filter ?(naming=Misctypes.IntroAnonymous) rigid = let evd', s = new_sort_variable rigid evd in - let evd', e = new_evar env evd' ?src ?filter (mkSort s) in + let evd', e = new_evar env evd' ?src ?filter ~naming (mkSort s) in evd', (e, s) -let e_new_type_evar env evdref ?src ?filter rigid = - let evd', c = new_type_evar env !evdref ?src ?filter rigid in +let e_new_type_evar env evdref ?src ?filter ?(naming=Misctypes.IntroAnonymous) rigid = + let evd', c = new_type_evar env !evdref ?src ?filter ~naming rigid in evdref := evd'; c @@ -399,8 +399,8 @@ let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = evdref := evd'; mkSort s (* The same using side-effect *) -let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ty = - let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ty in +let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) ty = + let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ~naming ty in evdref := evd'; ev diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 8a07cce5d..de55a643a 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -23,27 +23,32 @@ val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) val new_evar : env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> types -> evar_map * constr + ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> types -> evar_map * constr val new_pure_evar : named_context_val -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> types -> evar_map * evar + ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> types -> evar_map * evar val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar (** the same with side-effects *) val e_new_evar : env -> evar_map ref -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> - ?candidates:constr list -> ?store:Store.t -> types -> constr + ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> types -> constr (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : - env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> rigid -> + env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> rigid -> evar_map * (constr * sorts) val e_new_type_evar : env -> evar_map ref -> - ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> rigid -> constr * sorts + ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> rigid -> constr * sorts val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr @@ -65,7 +70,8 @@ val e_new_global : evar_map ref -> Globnames.global_reference -> constr val new_evar_instance : named_context_val -> evar_map -> types -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t -> ?candidates:constr list -> - ?store:Store.t -> constr list -> evar_map * constr + ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> + constr list -> evar_map * constr val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list diff --git a/pretyping/evd.ml b/pretyping/evd.ml index fd104d847..ffc1ea2a7 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -599,16 +599,28 @@ let progress_evar_map d1 d2 = in not (d1 == d2) && EvMap.exists is_new d1.undf_evars -let add_name_newly_undefined evk evi (evtoid,idtoev) = - let id = evar_ident_info evi in - let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in - (EvMap.add evk id evtoid, Idmap.add id evk idtoev) - -let add_name_undefined evk evi (evtoid,idtoev as evar_names) = +let add_name_newly_undefined naming evk evi (evtoid,idtoev) = + let id = match naming with + | Misctypes.IntroAnonymous -> + let id = evar_ident_info evi in + Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) + | Misctypes.IntroIdentifier id -> + let id' = + Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in + if not (Names.Id.equal id id') then + user_err_loc + (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id); + id' + | Misctypes.IntroFresh id -> + Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) + | Misctypes.IntroWildcard -> assert false in + (EvMap.add evk id evtoid, Idmap.add id evk idtoev) + +let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) = if EvMap.mem evk evtoid then evar_names else - add_name_newly_undefined evk evi evar_names + add_name_newly_undefined naming evk evi evar_names let remove_name_defined evk (evtoid,idtoev) = let id = EvMap.find evk evtoid in @@ -618,6 +630,14 @@ let remove_name_possibly_already_defined evk evar_names = try remove_name_defined evk evar_names with Not_found -> evar_names +let rename evk id evd = + let (evtoid,idtoev) = evd.evar_names in + let id' = EvMap.find evk evtoid in + if Idmap.mem id idtoev then anomaly (str "Evar name already in use"); + { evd with evar_names = + (EvMap.add evk id evtoid (* overwrite old name *), + Idmap.add id evk (Idmap.remove id' idtoev)) } + let reassign_name_defined evk evk' (evtoid,idtoev) = let id = EvMap.find evk evtoid in (EvMap.add evk' id (EvMap.remove evk evtoid), @@ -625,7 +645,7 @@ let reassign_name_defined evk evk' (evtoid,idtoev) = let add d e i = match i.evar_body with | Evar_empty -> - let evar_names = add_name_undefined e i d.evar_names in + let evar_names = add_name_undefined Misctypes.IntroAnonymous e i d.evar_names in { d with undf_evars = EvMap.add e i d.undf_evars; evar_names } | Evar_defined _ -> let evar_names = remove_name_possibly_already_defined e d.evar_names in @@ -839,7 +859,8 @@ let define evk body evd = { evd with defn_evars; undf_evars; last_mods; evar_names } let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) - ?(filter=Filter.identity) ?candidates ?(store=Store.empty) evd = + ?(filter=Filter.identity) ?candidates ?(store=Store.empty) + ?(naming=Misctypes.IntroAnonymous) evd = let () = match Filter.repr filter with | None -> () | Some filter -> @@ -854,7 +875,7 @@ let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) evar_candidates = candidates; evar_extra = store; } in - let evar_names = add_name_newly_undefined evk evar_info evd.evar_names in + let evar_names = add_name_newly_undefined naming evk evar_info evd.evar_names in { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; evar_names } let restrict evk evk' filter ?candidates evd = @@ -1018,7 +1039,7 @@ let merge_names evar_names def' undef' = EvMap.fold (fun n _ evar_names -> remove_name_possibly_already_defined n evar_names) def' evar_names in - EvMap.fold add_name_undefined undef' evar_names + EvMap.fold (add_name_undefined Misctypes.IntroAnonymous) undef' evar_names let merge_metas metas1 metas2 = List.fold_left (fun m (n,v) -> Metamap.add n v m) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 22768fb69..467e1a163 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -246,8 +246,8 @@ val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> val evar_declare : named_context_val -> evar -> types -> ?src:Loc.t * Evar_kinds.t -> - ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> - evar_map -> evar_map + ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> + ?naming:Misctypes.intro_pattern_naming_expr -> evar_map -> evar_map (** Convenience function. Just a wrapper around {!add}. *) val restrict : evar -> evar -> Filter.t -> ?candidates:constr list -> @@ -259,6 +259,8 @@ val evar_source : existential_key -> evar_map -> Evar_kinds.t located val evar_ident : existential_key -> evar_map -> Id.t +val rename : existential_key -> Id.t -> evar_map -> evar_map + val evar_key : Id.t -> evar_map -> existential_key val evar_source_of_meta : metavariable -> evar_map -> Evar_kinds.t located diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 9157cdb81..fd51545b2 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -96,8 +96,9 @@ let rec glob_constr_eq c1 c2 = match c1, c2 with Array.equal glob_constr_eq c1 c2 && Array.equal glob_constr_eq t1 t2 | GSort (_, s1), GSort (_, s2) -> Miscops.glob_sort_eq s1 s2 -| GHole (_, kn1, gn1), GHole (_, kn2, gn2) -> - Option.equal (==) gn1 gn2 (** Only thing sensible *) +| GHole (_, kn1, nam1, gn1), GHole (_, kn2, nam2, gn2) -> + Option.equal (==) gn1 gn2 (** Only thing sensible *) && + Miscops.intro_pattern_naming_eq nam1 nam2 | GCast (_, c1, t1), GCast (_, c2, t2) -> glob_constr_eq c1 c2 && cast_type_eq glob_constr_eq t1 t2 | _ -> false @@ -342,7 +343,7 @@ let loc_of_glob_constr = function | GIf (loc,_,_,_,_) -> loc | GRec (loc,_,_,_,_,_) -> loc | GSort (loc,_) -> loc - | GHole (loc,_,_) -> loc + | GHole (loc,_,_,_) -> loc | GCast (loc,_,_) -> loc (**********************************************************************) @@ -356,7 +357,7 @@ let rec cases_pattern_of_glob_constr na = function raise Not_found | Anonymous -> PatVar (loc,Name id) end - | GHole (loc,_,_) -> PatVar (loc,na) + | GHole (loc,_,_,_) -> PatVar (loc,na) | GRef (loc,ConstructRef cstr,_) -> PatCstr (loc,cstr,[],na) | GApp (loc,GRef (_,ConstructRef cstr,_),l) -> diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 5b5bbe095..e96e3a8b7 100644 --- a/pretyping/miscops.ml +++ b/pretyping/miscops.ml @@ -30,3 +30,10 @@ let glob_sort_eq g1 g2 = match g1, g2 with | GSet, GSet -> true | GType l1, GType l2 -> List.for_all2 CString.equal l1 l2 | _ -> false + +let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with +| IntroAnonymous, IntroAnonymous -> true +| IntroIdentifier id1, IntroIdentifier id2 -> Names.Id.equal id1 id2 +| IntroWildcard, IntroWildcard -> true +| IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2 +| _ -> false diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli index 84541a3b2..6235533d7 100644 --- a/pretyping/miscops.mli +++ b/pretyping/miscops.mli @@ -16,3 +16,8 @@ val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type (** Equalities on [glob_sort] *) val glob_sort_eq : glob_sort -> glob_sort -> bool + +(** Equalities on [intro_pattern_naming] *) + +val intro_pattern_naming_eq : + intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 4a1dc1dd6..3e43853a5 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -355,7 +355,7 @@ let rec pat_of_raw metas vars = function pat_of_raw metas vars b1,pat_of_raw metas vars b2) | GLetTuple (loc,nal,(_,None),b,c) -> let mkGLambda c na = - GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, None),c) in + GLambda (loc,na,Explicit,GHole (loc,Evar_kinds.InternalHole, IntroAnonymous, None),c) in let c = List.fold_left mkGLambda c nal in let cip = { cip_style = LetStyle; diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8c4dbfd98..69aee0a60 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -440,15 +440,15 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var let k = Evar_kinds.MatchingVar (someta,n) in { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } - | GHole (loc, k, None) -> + | GHole (loc, k, naming, None) -> let ty = match tycon with | Some ty -> ty | None -> new_type_evar env evdref loc in - { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } + { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty } - | GHole (loc, k, Some arg) -> + | GHole (loc, k, _naming, Some arg) -> let ty = match tycon with | Some ty -> ty @@ -910,7 +910,7 @@ and pretype_instance resolve_tc env evdref lvar loc hyps evk update = (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) and pretype_type resolve_tc valcon env evdref lvar = function - | GHole (loc, knd, None) -> + | GHole (loc, knd, naming, None) -> (match valcon with | Some v -> let s = @@ -926,7 +926,7 @@ and pretype_type resolve_tc valcon env evdref lvar = function utj_type = s } | None -> let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in - { utj_val = e_new_evar env evdref ~src:(loc, knd) (mkSort s); + { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s); utj_type = s}) | c -> let j = pretype resolve_tc empty_tycon env evdref lvar c in -- cgit v1.2.3