diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/locusops.ml | 22 | ||||
| -rw-r--r-- | pretyping/locusops.mli | 9 | ||||
| -rw-r--r-- | pretyping/unification.ml | 21 | ||||
| -rw-r--r-- | pretyping/unification.mli | 2 |
4 files changed, 30 insertions, 24 deletions
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 21157d9d5a..7e825b6c24 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -87,22 +87,22 @@ let out_arg = function | Misctypes.ArgVar _ -> Errors.anomaly (Pp.str "Unevaluated or_var variable") | Misctypes.ArgArg x -> x -let occurrences_of_hyp id =function - | LikeFirst -> LikeFirst - | AtOccs cls -> +let occurrences_of_hyp id cls = let rec hyp_occ = function [] -> NoOccurrences, InHyp | ((occs,id'),hl)::_ when Names.Id.equal id id' -> occurrences_map (List.map out_arg) occs, hl | _::l -> hyp_occ l in - AtOccs (match cls.onhyps with + match cls.onhyps with None -> AllOccurrences,InHyp - | Some l -> hyp_occ l) + | Some l -> hyp_occ l -let occurrences_of_goal = function - | LikeFirst -> LikeFirst - | AtOccs cls -> AtOccs (occurrences_map (List.map out_arg) cls.concl_occs) +let occurrences_of_goal cls = + occurrences_map (List.map out_arg) cls.concl_occs -let in_every_hyp = function - | LikeFirst -> true - | AtOccs cls -> Option.is_empty cls.onhyps +let in_every_hyp cls = Option.is_empty cls.onhyps + +let has_selected_occurrences cls = + cls.concl_occs != AllOccurrences || + not (Option.is_empty cls.onhyps) && List.exists (fun ((occs,_),hl) -> + occs != AllOccurrences || hl != InHyp) (Option.get cls.onhyps) diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index f6d27a1850..c1bf2d9eae 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -38,7 +38,8 @@ val concrete_clause_of : (unit -> Id.t list) -> clause -> concrete_clause (** Miscellaneous functions *) -val occurrences_of_hyp : Id.t -> clause or_like_first -> - (occurrences * hyp_location_flag) or_like_first -val occurrences_of_goal : clause or_like_first -> occurrences or_like_first -val in_every_hyp : clause or_like_first -> bool +val occurrences_of_hyp : Id.t -> clause -> (occurrences * hyp_location_flag) +val occurrences_of_goal : clause -> occurrences +val in_every_hyp : clause -> bool + +val has_selected_occurrences : clause -> bool diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 07940bf57d..3f2963bfe5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1468,10 +1468,11 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = else x in + let likefirst = not (has_selected_occurrences occs) in let mkvarid () = mkVar id in let compute_dependency _ (hyp,_,_ as d) (sign,depdecls) = match occurrences_of_hyp hyp occs with - | AtOccs (NoOccurrences, InHyp) -> + | NoOccurrences, InHyp -> if indirectly_dependent c d depdecls then (* Told explicitly not to abstract over [d], but it is dependent *) let id' = indirect_dependency d depdecls in @@ -1480,8 +1481,9 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = ++ str ".") else (push_named_context_val d sign,depdecls) - | (AtOccs (AllOccurrences, InHyp) | LikeFirst) -> - let newdecl = replace_term_occ_decl_modulo LikeFirst test mkvarid d in + | AllOccurrences, InHyp as occ -> + let occ = if likefirst then LikeFirst else AtOccs occ in + let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in if Context.eq_named_declaration d newdecl && not (indirectly_dependent c d depdecls) then @@ -1491,15 +1493,18 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = else (push_named_context_val newdecl sign, newdecl :: depdecls) | occ -> - let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in + (* There are specific occurrences, hence not like first *) + let newdecl = replace_term_occ_decl_modulo (AtOccs occ) test mkvarid d in (push_named_context_val newdecl sign, newdecl :: depdecls) in try let sign,depdecls = fold_named_context compute_dependency env ~init:(empty_named_context_val,[]) in let ccl = match occurrences_of_goal occs with - | AtOccs NoOccurrences -> concl - | occ -> replace_term_occ_modulo occ test mkvarid concl + | NoOccurrences -> concl + | occ -> + let occ = if likefirst then LikeFirst else AtOccs occ in + replace_term_occ_modulo occ test mkvarid concl in let lastlhyp = if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in @@ -1522,7 +1527,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = type prefix_of_inductive_support_flag = bool type abstraction_request = -| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause or_like_first * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Name.t * pending_constr * clause * bool | AbstractExact of Name.t * constr * types option * clause * bool type abstraction_result = @@ -1539,7 +1544,7 @@ let make_abstraction env evd ccl abs = | AbstractExact (name,c,ty,occs,check_occs) -> make_abstraction_core name (make_eq_test env evd c) - env evd c ty (AtOccs occs) check_occs ccl + env evd c ty occs check_occs ccl let keyed_unify env evd kop = if not !keyed_unification then fun cl -> true diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 7f5cac2d23..0f5a62bb5f 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -68,7 +68,7 @@ exception PatternNotFound type prefix_of_inductive_support_flag = bool type abstraction_request = -| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause Locus.or_like_first * bool +| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause * bool | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool val finish_evar_resolution : ?flags:Pretyping.inference_flags -> |