aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-08-29 14:41:47 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-10-13 19:12:34 +0200
commit56cb514b425360ca428be116e9ea1d5205edd06f (patch)
tree2edec11d80f78c0caeae35913fa156768b9d3536 /pretyping
parentc72eb85062edea223f5868c67ded99da7954d49a (diff)
Moving function about locs in locusops.
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/locusops.ml21
-rw-r--r--pretyping/locusops.mli7
-rw-r--r--pretyping/unification.ml31
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