summaryrefslogtreecommitdiff
path: root/pretyping/find_subterm.mli
blob: 47d9654e579b876d6c81a37597bc12ebe4ded6b1 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Locus
open Context
open Term
open Evd
open Pretype_errors
open Environ

(** Finding subterms, possibly up to some unification function,
    possibly at some given occurrences *)

exception NotUnifiable of (constr * constr * unification_error) option

exception SubtermUnificationError of subterm_unification_error

(** A testing function is typically a unification function returning a
    substitution or failing with a NotUnifiable error, together with a
    function to merge substitutions and an initial substitution;
    last_found is used for error messages and it has to be initialized
    with None. *)

type 'a testing_function = {
  match_fun : 'a -> constr -> 'a;
  merge_fun : 'a -> 'a -> 'a;
  mutable testing_state : 'a;
  mutable last_found : position_reporting option
}

(** This is the basic testing function, looking for exact matches of a
    closed term *)
val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function

(** [replace_term_occ_modulo occl test mk c] looks in [c] for subterm
    modulo a testing function [test] and replaces successfully
    matching subterms at the indicated occurrences [occl] with [mk
    ()]; it turns a NotUnifiable exception raised by the testing
    function into a SubtermUnificationError. *)
val replace_term_occ_modulo : occurrences or_like_first ->
  'a testing_function -> (unit -> constr) -> constr -> constr

(** [replace_term_occ_decl_modulo] is similar to
    [replace_term_occ_modulo] but for a named_declaration. *)
val replace_term_occ_decl_modulo :
  (occurrences * hyp_location_flag) or_like_first ->
  'a testing_function -> (unit -> constr) ->
  named_declaration -> named_declaration

(** [subst_closed_term_occ occl c d] replaces occurrences of
    closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC),
    unifying universes which results in a set of constraints. *)
val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first ->
  constr -> constr -> constr * evar_map

(** [subst_closed_term_occ_decl evd occl c decl] replaces occurrences of 
    closed [c] at positions [occl] by [Rel 1] in [decl]. *)
val subst_closed_term_occ_decl : env -> evar_map ->
  (occurrences * hyp_location_flag) or_like_first ->
  constr -> named_declaration -> named_declaration * evar_map

(** Miscellaneous *)
val error_invalid_occurrence : int list -> 'a