diff options
| -rw-r--r-- | plugins/subtac/subtac_cases.ml | 2 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 2 | ||||
| -rw-r--r-- | pretyping/termops.ml | 106 | ||||
| -rw-r--r-- | pretyping/termops.mli | 35 | ||||
| -rw-r--r-- | pretyping/unification.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 28 |
6 files changed, 94 insertions, 81 deletions
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 68e4e7224..368d8bac3 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -1783,7 +1783,7 @@ let abstract_tomatch env tomatchs tycon = Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names, tycon | _ -> let tycon = Option.map - (fun t -> subst_term_occ all_occurrences (lift 1 c) (lift 1 t)) tycon in + (fun t -> subst_term (lift 1 c) (lift 1 t)) tycon in let name = next_ident_away (id_of_string "filtered_var") names in (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev, (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx, diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 715fc2360..b6c67555d 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -854,7 +854,7 @@ let abstract_scheme env sigma (locc,a) c = if occur_meta a then mkLambda (na,ta,c) else - mkLambda (na,ta,subst_term_occ locc a c) + mkLambda (na,ta,subst_closed_term_occ locc a c) let pattern_occs loccs_trm env sigma c = let abstr_trm = List.fold_right (abstract_scheme env sigma) loccs_trm c in diff --git a/pretyping/termops.ml b/pretyping/termops.ml index b10d8e935..9e8d22a87 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -622,10 +622,8 @@ let my_prefix_application eq_fun (k,c) (by_c : constr) (t : constr) = None | _ -> None -(* Recognizing occurrences of a given (closed) subterm in a term for Pattern : - [subst_term c t] substitutes [(Rel 1)] for all occurrences of (closed) - term [c] in a term [t] *) -(*i Bizarre : si on cherche un sous terme clos, pourquoi le lifter ? i*) +(* Recognizing occurrences of a given subterm in a term: [subst_term c t] + substitutes [(Rel 1)] for all occurrences of term [c] in a term [t] *) let subst_term_gen eq_fun c t = let rec substrec (k,c as kc) t = @@ -638,8 +636,8 @@ let subst_term_gen eq_fun c t = in substrec (1,c) t -(* Recognizing occurrences of a given (closed) subterm in a term : - [replace_term c1 c2 t] substitutes [c2] for all occurrences of (closed) +(* Recognizing occurrences of a given subterm in a term : + [replace_term c1 c2 t] substitutes [c2] for all occurrences of term [c1] in a term [t] *) (*i Meme remarque : a priori [c] n'est pas forcement clos i*) @@ -689,64 +687,88 @@ let is_selected pos (nowhere_except_in,locs) = nowhere_except_in && List.mem pos locs || not nowhere_except_in && not (List.mem pos locs) -let subst_term_occ_gen_modulo (nowhere_except_in,locs as plocs) - unify_fun merge_fun substs occ c t = +exception NotUnifiable + +let subst_closed_term_occ_gen_modulo (nowhere_except_in,locs as plocs) + match_fun merge_fun substs occ t = let maxocc = List.fold_right max locs 0 in let pos = ref occ in let substs = ref substs in let add_subst subst = try substs := merge_fun subst !substs - with _ -> error_cannot_unify_occurrences !pos plocs in - assert (List.for_all (fun x -> x >= 0) locs); - let rec substrec (k,c as kc) t = + with NotUnifiable -> error_cannot_unify_occurrences !pos plocs in + let rec substrec k t = if nowhere_except_in & !pos > maxocc then t else try - let subst = unify_fun c t in + let subst = match_fun t in let r = if is_selected !pos plocs then (add_subst subst; mkRel k) else t in incr pos; r with _ -> - map_constr_with_binders_left_to_right - (fun d (k,c) -> (k+1,lift 1 c)) - substrec kc t + map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k t in - let t' = substrec (1,c) t in + let t' = substrec 1 t in (!substs,!pos, t') -let subst_term_occ_gen plocs pos c t = - let (_,pos,t) = subst_term_occ_gen_modulo plocs - (fun c1 c2 -> if eq_constr c1 c2 then () else raise Exit) - (fun () () -> ()) () pos c t in +let is_nowhere (nowhere_except_in,locs) = nowhere_except_in && locs = [] + +let check_used_occurrences nbocc (nowhere_except_in,locs) = + let rest = List.filter (fun o -> o >= nbocc) locs in + if rest <> [] then error_invalid_occurrence rest + +let proceed_with_occurrences f plocs x = + if is_nowhere plocs then (* optimization *) x else + begin + assert (List.for_all (fun x -> x >= 0) (snd plocs)); + let (nbocc,x) = f 1 x in + check_used_occurrences nbocc plocs; + x + end + +let subst_closed_term_occ_gen plocs pos c t = + let (_,pos,t) = subst_closed_term_occ_gen_modulo plocs + (fun c' -> if eq_constr c c' then () else raise Exit) + (fun () () -> ()) () pos t in (pos,t) -let subst_term_occ (nowhere_except_in,locs as plocs) c t = - if locs = [] then if nowhere_except_in then t else subst_term c t - else - let (nbocc,t') = subst_term_occ_gen plocs 1 c t in - let rest = List.filter (fun o -> o >= nbocc) locs in - if rest <> [] then error_invalid_occurrence rest; - t' +let subst_closed_term_occ plocs c t = + proceed_with_occurrences (fun occ -> subst_closed_term_occ_gen plocs occ c) + plocs t type hyp_location_flag = (* To distinguish body and type of local defs *) | InHyp | InHypTypeOnly | InHypValueOnly -let subst_term_occ_decl ((nowhere_except_in,locs as plocs),hloc) c (id,bodyopt,typ as d) = - match bodyopt,hloc with - | None, InHypValueOnly -> errorlabstrm "" (pr_id id ++ str " has no value") - | None, _ -> (id,None,subst_term_occ plocs c typ) - | Some body, InHypTypeOnly -> (id,Some body,subst_term_occ plocs c typ) - | Some body, InHypValueOnly -> (id,Some (subst_term_occ plocs c body),typ) +let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) = + match bodyopt,hyploc with + | None, InHypValueOnly -> + errorlabstrm "" (pr_id id ++ str " has no value.") + | None, _ | Some _, InHypTypeOnly -> + let acc,typ = f acc typ in acc,(id,bodyopt,typ) + | Some body, InHypValueOnly -> + let acc,body = f acc body in acc,(id,Some body,typ) | Some body, InHyp -> - if locs = [] then - if nowhere_except_in then d - else (id,Some (subst_term c body),subst_term c typ) - else - let (nbocc,body') = subst_term_occ_gen plocs 1 c body in - let (nbocc',t') = subst_term_occ_gen plocs nbocc c typ in - let rest = List.filter (fun o -> o >= nbocc') locs in - if rest <> [] then error_invalid_occurrence rest; - (id,Some body',t') + let acc,body = f acc body in + let acc,typ = f acc typ in + acc,(id,Some body,typ) + +let subst_closed_term_occ_decl (plocs,hyploc) c d = + proceed_with_occurrences + (map_named_declaration_with_hyploc + (fun occ -> subst_closed_term_occ_gen plocs occ c) hyploc) plocs d + +let subst_closed_term_occ_decl_modulo (plocs,hyploc) + match_fun merge_fun substs d = + let subst = ref substs in + proceed_with_occurrences + (map_named_declaration_with_hyploc + (fun occ t -> + let (substs,occ,t) = + subst_closed_term_occ_gen_modulo plocs + match_fun merge_fun !subst occ t + in subst := substs; (occ,t)) + hyploc) + plocs d let vars_of_env env = let s = diff --git a/pretyping/termops.mli b/pretyping/termops.mli index c74551735..2e202bf07 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -148,34 +148,43 @@ type occurrences = bool * int list val all_occurrences : occurrences val no_occurrences_in_set : occurrences -(** [subst_term_occ_gen occl n c d] replaces occurrences of [c] at +(** [subst_closed_term_occ_gen occl n c d] replaces occurrences of closed [c] at positions [occl], counting from [n], by [Rel 1] in [d] *) -val subst_term_occ_gen : +val subst_closed_term_occ_gen : occurrences -> int -> constr -> types -> int * types -(** [subst_term_occ_gen_modulo] looks for subterm modulo a comparison - function returning a substitution of type ['a]; a function for - merging substitution and an initial substitution are required too *) -val subst_term_occ_gen_modulo : - occurrences -> (constr -> constr -> 'a) -> ('a -> 'a -> 'a) -> 'a -> - int -> constr -> types -> 'a * int * types +(** [subst_closed_term_occ_gen_modulo] looks for subterm modulo a + testing function returning a substitution of type ['a] (or failing + with NotUnifiable); a function for merging substitution (possibly + failing with NotUnifiable) and an initial substitution are + required too *) -(** [subst_term_occ occl c d] replaces occurrences of [c] at +exception NotUnifiable + +val subst_closed_term_occ_gen_modulo : + occurrences -> (constr -> 'a) -> ('a -> 'a -> 'a) -> 'a -> + int -> constr -> 'a * int * types + +(** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC) *) -val subst_term_occ : occurrences -> constr -> constr -> constr +val subst_closed_term_occ : occurrences -> constr -> constr -> constr -(** [subst_term_occ_decl occl c decl] replaces occurrences of [c] at - positions [occl] by [Rel 1] in [decl] *) +(** [subst_closed_term_occ_decl occl c decl] replaces occurrences of closed [c] + at positions [occl] by [Rel 1] in [decl] *) type hyp_location_flag = (** To distinguish body and type of local defs *) | InHyp | InHypTypeOnly | InHypValueOnly -val subst_term_occ_decl : +val subst_closed_term_occ_decl : occurrences * hyp_location_flag -> constr -> named_declaration -> named_declaration +val subst_closed_term_occ_decl_modulo : + occurrences * hyp_location_flag -> (constr -> 'a) -> ('a -> 'a -> 'a) -> 'a -> + named_declaration -> named_declaration + val error_invalid_occurrence : int list -> 'a (** Alternative term equalities *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 4610c06ce..4a873f1f9 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -49,7 +49,7 @@ let abstract_scheme env c l lname_typ = are unclear... if occur_meta ta then error "cannot find a type for the generalisation" else *) if occur_meta a then mkLambda_name env (na,ta,t) - else mkLambda_name env (na,ta,subst_term_occ locc a t)) + else mkLambda_name env (na,ta,subst_closed_term_occ locc a t)) c (List.rev l) lname_typ diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 1cc5c585d..5e4abb726 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1485,7 +1485,7 @@ let generalize_goal gl i ((occs,c,b),na) cl = let decls,cl = decompose_prod_n_assum i cl in let dummy_prod = it_mkProd_or_LetIn mkProp decls in let newdecls,_ = decompose_prod_n_assum i (subst_term c dummy_prod) in - let cl' = subst_term_occ occs c (it_mkProd_or_LetIn cl newdecls) in + let cl' = subst_closed_term_occ occs c (it_mkProd_or_LetIn cl newdecls) in let na = generalized_name c t (pf_ids_of_hyps gl) cl' na in mkProd_or_LetIn (na,b,t) cl' @@ -1660,33 +1660,14 @@ let letin_tac with_eq name c occs gl = (* Implementation without generalisation: abbrev will be lost in hyps in *) (* in the extracted proof *) -let default_matching_flags = { - modulo_conv_on_closed_terms = Some empty_transparent_state; - use_metas_eagerly_in_conv_on_closed_terms = false; - modulo_delta = empty_transparent_state; - modulo_delta_types = full_transparent_state; - resolve_evars = false; - use_pattern_unification = false; - use_meta_bound_pattern_unification = false; - frozen_evars = ExistentialSet.empty; - restrict_conv_on_strict_subterms = false; - modulo_betaiota = false; - modulo_eta = false; - allow_K_in_toplevel_higher_order_unification = false -} - -let matching_fun sigma c1 c2 = - w_unify false env CONV flags:default_matching_flags - - let letin_abstract id c (occs,check_occs) gl = let env = pf_env gl in let compute_dependency _ (hyp,_,_ as d) depdecls = match occurrences_of_hyp hyp occs with | None -> depdecls | Some occ -> - let newdecl = subst_term_occ_decl occ c d in - if occ = (all_occurrences,InHyp) && eq_named_declaration d newdecl then + let newdecl = subst_closed_term_occ_decl occ c d in + if occ = (all_occurrences,InHyp) & eq_named_declaration d newdecl then if check_occs & not (in_every_hyp occs) then raise (RefinerError (DoesNotOccurIn (c,hyp))) else depdecls @@ -1695,7 +1676,8 @@ let letin_abstract id c (occs,check_occs) gl = let depdecls = fold_named_context compute_dependency env ~init:[] in let ccl = match occurrences_of_goal occs with | None -> pf_concl gl - | Some occ -> subst1 (mkVar id) (subst_term_occ occ c (pf_concl gl)) in + | Some occ -> subst1 (mkVar id) (subst_closed_term_occ occ c (pf_concl gl)) + in let lastlhyp = if depdecls = [] then no_move else MoveAfter(pi1(list_last depdecls)) in (depdecls,lastlhyp,ccl) |