diff options
| -rw-r--r-- | pretyping/locusops.ml | 21 | ||||
| -rw-r--r-- | pretyping/locusops.mli | 7 | ||||
| -rw-r--r-- | pretyping/unification.ml | 31 |
3 files changed, 33 insertions, 26 deletions
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 3bbd8af44..5484c8095 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -80,3 +80,24 @@ let concrete_clause_of enum_hyps cl = if cl.concl_occs = NoOccurrences then hyps else OnConcl cl.concl_occs :: hyps + +(** Miscellaneous functions *) + +let out_arg = function + | Misctypes.ArgVar _ -> Errors.anomaly (Pp.str "Unevaluated or_var variable") + | Misctypes.ArgArg x -> x + +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 + match cls.onhyps with + None -> AllOccurrences,InHyp + | Some l -> hyp_occ l + +let occurrences_of_goal cls = + occurrences_map (List.map out_arg) cls.concl_occs + +let in_every_hyp cls = Option.is_empty cls.onhyps diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index a086a6f58..73d13c0bc 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -35,3 +35,10 @@ val is_nowhere : 'a clause_expr -> bool val simple_clause_of : (unit -> Id.t list) -> clause -> simple_clause val concrete_clause_of : (unit -> Id.t list) -> clause -> concrete_clause + +(** Miscellaneous functions *) + +val occurrences_of_hyp : Id.t -> Id.t clause_expr -> + occurrences * hyp_location_flag +val occurrences_of_goal : 'a clause_expr -> occurrences +val in_every_hyp : 'a clause_expr -> bool diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 2a6fd6fe7..7544ba37a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1311,26 +1311,6 @@ let iter_fail f a = (* make_abstraction: a variant of w_unify_to_subterm which works on contexts, with evars, and possibly with occurrences *) -let out_arg = function - | Misctypes.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") - | Misctypes.ArgArg x -> x - -let occurrences_of_hyp id cls = - let rec hyp_occ = function - [] -> None - | ((occs,id'),hl)::_ when Id.equal id id' -> - Some (occurrences_map (List.map out_arg) occs, hl) - | _::l -> hyp_occ l in - match cls.onhyps with - None -> Some (AllOccurrences,InHyp) - | Some l -> hyp_occ l - -let occurrences_of_goal cls = - if cls.concl_occs == NoOccurrences then None - else Some (occurrences_map (List.map out_arg) cls.concl_occs) - -let in_every_hyp cls = Option.is_empty cls.onhyps - let indirectly_dependent c d decls = not (isVar c) && (* This test is not needed if the original term is a variable, but @@ -1432,7 +1412,7 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc let mkvarid () = mkVar id in let compute_dependency _ (hyp,_,_ as d) depdecls = match occurrences_of_hyp hyp occs with - | None -> + | 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 @@ -1441,7 +1421,7 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc ++ str ".") else depdecls - | Some ((AllOccurrences, InHyp) as occ) -> + | (AllOccurrences, InHyp) as occ -> 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) @@ -1451,14 +1431,13 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc else depdecls else newdecl :: depdecls - | Some occ -> + | occ -> replace_term_occ_decl_modulo occ test mkvarid d :: depdecls in try let depdecls = fold_named_context compute_dependency env ~init:[] in let ccl = match occurrences_of_goal occs with - | None -> concl - | Some occ -> - replace_term_occ_modulo occ test mkvarid concl + | NoOccurrences -> concl + | occ -> 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 |