(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (* * (see LICENSE file for the text of the license) *) (************************************************************************)
open Pp open CErrors open Names open Locus open EConstr open Termops open Pretype_errors
module NamedDecl = Context.Named.Declaration
(** Processing occurrences *)
let explain_incorrect_in_value_occurrence id =
Id.print id ++ str " has no value."
let proceed_with_occurrences f occs x = match occs with
| NoOccurrences -> x
| occs -> let (occs,x) = f (Locusops.initialize_occurrence_counter occs) x in
Locusops.check_used_occurrences occs;
x
(** Applying a function over a named_declaration with an hypothesis
location request *)
let map_named_declaration_with_hyploc f hyploc acc decl = letopen Context.Named.Declaration in let f acc typ = let acc, typ = f (Some (NamedDecl.get_id decl, hyploc)) acc typ in
acc, typ in match decl,hyploc with
| LocalAssum (id,_), InHypValueOnly ->
user_err (explain_incorrect_in_value_occurrence id.Context.binder_name)
| LocalAssum (id,typ), _ -> let acc,typ = f acc typ in acc, LocalAssum (id,typ)
| LocalDef (id,body,typ), InHypTypeOnly -> let acc,typ = f acc typ in acc, LocalDef (id,body,typ)
| LocalDef (id,body,typ), InHypValueOnly -> let acc,body = f acc body in acc, LocalDef (id,body,typ)
| LocalDef (id,body,typ), InHyp -> let acc,body = f acc body in let acc,typ = f acc typ in
acc, LocalDef (id,body,typ)
(** Finding a subterm up to some testing function *)
exception SubtermUnificationError of subterm_unification_error
type ('a, 'b) testing_function = {
match_fun : int -> 'a -> EConstr.constr -> ('b, unit) Result.t;
merge_fun : 'b -> 'a -> ('a, unit) Result.t;
mutable testing_state : 'a;
mutable last_found : position_reporting option
}
(* Find subterms using a testing function, but only at a list of locations or excluding a list of locations; in the occurrences list (b,l), b=true means no occurrence except the ones in l and b=false,
means all occurrences except the ones in l *)
let replace_term_occ_gen_modulo env sigma like_first test bywhat cl count t = let count = ref count in let rec substrec (nested, k) t = if Locusops.occurrences_done !count then t else matchtest.match_fun k test.testing_state t with
| Result.Ok subst -> let selected, count' = Locusops.update_occurrence_counter !count in let () = count := count' in if selected then let pos = Locusops.current_occurrence !count in if nested then (* in case it is nested but not later detected as unconvertible,
as when matching "id _" in "id (id 0)" *) let lastpos = Option.get test.last_found in raise (SubtermUnificationError (nested, ((cl, pos), t), lastpos)) elsematchtest.merge_fun subst test.testing_state with
| Result.Ok state -> let () = test.testing_state <- state in let () = test.last_found <- Some ((cl, pos), t) in (* Check nested matching subterms *) let () = if Locusops.more_specific_occurrences !count then
ignore (subst_below (true, k) t) in
Vars.lift k (bywhat ())
| Result.Error () -> if like_first then subst_below (nested, k) t else let lastpos = Option.get test.last_found in raise (SubtermUnificationError (nested, ((cl, pos), t), lastpos)) else
subst_below (nested, k) t
| Result.Error () ->
subst_below (nested, k) t and subst_below k t =
map_constr_with_binders_left_to_right env sigma (fun d (nested, k) -> (nested, k + 1)) substrec k t in let t' = substrec (false, 0) t in
(!count, t')
let replace_term_occ_modulo env evd occs test bywhat t = let occs',like_first = match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,truein
proceed_with_occurrences
(replace_term_occ_gen_modulo env evd like_first test bywhat None) occs' t
let replace_term_occ_decl_modulo env evd occs test bywhat d = let (plocs,hyploc),like_first = match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),truein
proceed_with_occurrences
(map_named_declaration_with_hyploc
(replace_term_occ_gen_modulo env evd like_first test bywhat)
hyploc)
plocs d
(** Finding an exact subterm *)
let make_eq_univs_test env evd c =
{ match_fun = (fun k evd c' -> match EConstr.eq_constr_universes_proj env evd c c' with
| None -> Result.Error ()
| Some cst -> try Result.Ok (Evd.add_universe_constraints evd cst) with Evd.UniversesDiffer | UGraph.UniverseInconsistency _ -> Result.Error ()
);
merge_fun = (fun evd _ -> Result.Ok evd);
testing_state = evd;
last_found = None
}
let subst_closed_term_occ env evd occs c t = lettest = make_eq_univs_test env evd c in let bywhat () = mkRel 1 in let t' = replace_term_occ_modulo env evd occs test bywhat t in
t', test.testing_state
let subst_closed_term_occ_decl env evd occs c d = lettest = make_eq_univs_test env evd c in let (plocs,hyploc),like_first = match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),truein let bywhat () = mkRel 1 in
proceed_with_occurrences
(map_named_declaration_with_hyploc
(fun _ -> replace_term_occ_gen_modulo env evd like_first test bywhat None)
hyploc) plocs d, test.testing_state
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
