From 1b92c226e563643da187b8614d5888dc4855eb43 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- plugins/ssrmatching/ssrmatching.mli | 241 ++++++++++++++++++++++++++++++++++++ 1 file changed, 241 insertions(+) create mode 100644 plugins/ssrmatching/ssrmatching.mli (limited to 'plugins/ssrmatching/ssrmatching.mli') diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli new file mode 100644 index 00000000..288a04e6 --- /dev/null +++ b/plugins/ssrmatching/ssrmatching.mli @@ -0,0 +1,241 @@ +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) +(* Distributed under the terms of CeCILL-B. *) + +open Genarg +open Tacexpr +open Environ +open Tacmach +open Evd +open Proof_type +open Term + +(** ******** Small Scale Reflection pattern matching facilities ************* *) + +(** Pattern parsing *) + +(** The type of context patterns, the patterns of the [set] tactic and + [:] tactical. These are patterns that identify a precise subterm. *) +type cpattern +val pr_cpattern : cpattern -> Pp.std_ppcmds + +(** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *) +val cpattern : cpattern Pcoq.Gram.entry +val wit_cpattern : cpattern uniform_genarg_type + +(** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *) +val lcpattern : cpattern Pcoq.Gram.entry +val wit_lcpattern : cpattern uniform_genarg_type + +(** The type of rewrite patterns, the patterns of the [rewrite] tactic. + These patterns also include patterns that identify all the subterms + of a context (i.e. "in" prefix) *) +type rpattern +val pr_rpattern : rpattern -> Pp.std_ppcmds + +(** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *) +val rpattern : rpattern Pcoq.Gram.entry +val wit_rpattern : rpattern uniform_genarg_type + +(** Pattern interpretation and matching *) + +exception NoMatch +exception NoProgress + +(** AST for [rpattern] (and consequently [cpattern]) *) +type ('ident, 'term) ssrpattern = + | T of 'term + | In_T of 'term + | X_In_T of 'ident * 'term + | In_X_In_T of 'ident * 'term + | E_In_X_In_T of 'term * 'ident * 'term + | E_As_X_In_T of 'term * 'ident * 'term + +type pattern = evar_map * (constr, constr) ssrpattern +val pp_pattern : pattern -> Pp.std_ppcmds + +(** Extracts the redex and applies to it the substitution part of the pattern. + @raise Anomaly if called on [In_T] or [In_X_In_T] *) +val redex_of_pattern : + ?resolve_typeclasses:bool -> env -> pattern -> + constr Evd.in_evar_universe_context + +(** [interp_rpattern ise gl rpat] "internalizes" and "interprets" [rpat] + in the current [Ltac] interpretation signature [ise] and tactic input [gl]*) +val interp_rpattern : + Tacinterp.interp_sign -> goal sigma -> + rpattern -> + pattern + +(** [interp_cpattern ise gl cpat ty] "internalizes" and "interprets" [cpat] + in the current [Ltac] interpretation signature [ise] and tactic input [gl]. + [ty] is an optional type for the redex of [cpat] *) +val interp_cpattern : + Tacinterp.interp_sign -> goal sigma -> + cpattern -> glob_constr_and_expr option -> + pattern + +(** The set of occurrences to be matched. The boolean is set to true + * to signal the complement of this set (i.e. {-1 3}) *) +type occ = (bool * int list) option + +(** [subst e p t i]. [i] is the number of binders + traversed so far, [p] the term from the pattern, [t] the matched one *) +type subst = env -> constr -> constr -> int -> constr + +(** [eval_pattern b env sigma t pat occ subst] maps [t] calling [subst] on every + [occ] occurrence of [pat]. The [int] argument is the number of + binders traversed. If [pat] is [None] then then subst is called on [t]. + [t] must live in [env] and [sigma], [pat] must have been interpreted in + (an extension of) [sigma]. + @raise NoMatch if [pat] has no occurrence and [b] is [true] (default [false]) + @return [t] where all [occ] occurrences of [pat] have been mapped using + [subst] *) +val eval_pattern : + ?raise_NoMatch:bool -> + env -> evar_map -> constr -> + pattern option -> occ -> subst -> + constr + +(** [fill_occ_pattern b env sigma t pat occ h] is a simplified version of + [eval_pattern]. + It replaces all [occ] occurrences of [pat] in [t] with Rel [h]. + [t] must live in [env] and [sigma], [pat] must have been interpreted in + (an extension of) [sigma]. + @raise NoMatch if [pat] has no occurrence and [b] is [true] (default [false]) + @return the instance of the redex of [pat] that was matched and [t] + transformed as described above. *) +val fill_occ_pattern : + ?raise_NoMatch:bool -> + env -> evar_map -> constr -> + pattern -> occ -> int -> + constr Evd.in_evar_universe_context * constr + +(** *************************** Low level APIs ****************************** *) + +(* The primitive matching facility. It matches of a term with holes, like + the T pattern above, and calls a continuation on its occurrences. *) + +type ssrdir = L2R | R2L +val pr_dir_side : ssrdir -> Pp.std_ppcmds + +(** a pattern for a term with wildcards *) +type tpattern + +(** [mk_tpattern env sigma0 sigma_p ok p_origin dir t] compiles a term [t] + living in [env] [sigma] (an extension of [sigma0]) intro a [tpattern]. + The [tpattern] can hold a (proof) term [p] and a diction [dir]. The [ok] + callback is used to filter occurrences. + @return the compiled [tpattern] and its [evar_map] + @raise UserEerror is the pattern is a wildcard *) +val mk_tpattern : + ?p_origin:ssrdir * constr -> + env -> evar_map -> + evar_map * constr -> + (constr -> evar_map -> bool) -> + ssrdir -> constr -> + evar_map * tpattern + +(** [findP env t i k] is a stateful function that finds the next occurrence + of a tpattern and calls the callback [k] to map the subterm matched. + The [int] argument passed to [k] is the number of binders traversed so far + plus the initial value [i]. + @return [t] where the subterms identified by the selected occurrences of + the patter have been mapped using [k] + @raise NoMatch if the raise_NoMatch flag given to [mk_tpattern_matcher] is + [true] and if the pattern did not match + @raise UserEerror if the raise_NoMatch flag given to [mk_tpattern_matcher] is + [false] and if the pattern did not match *) +type find_P = + env -> constr -> int -> k:subst -> constr + +(** [conclude ()] asserts that all mentioned ocurrences have been visited. + @return the instance of the pattern, the evarmap after the pattern + instantiation, the proof term and the ssrdit stored in the tpattern + @raise UserEerror if too many occurrences were specified *) +type conclude = + unit -> constr * ssrdir * (evar_map * Evd.evar_universe_context * constr) + +(** [mk_tpattern_matcher b o sigma0 occ sigma_tplist] creates a pair + a function [find_P] and [conclude] with the behaviour explained above. + The flag [b] (default [false]) changes the error reporting behaviour + of [find_P] if none of the [tpattern] matches. The argument [o] can + be passed to tune the [UserError] eventually raised (useful if the + pattern is coming from the LHS/RHS of an equation) *) +val mk_tpattern_matcher : + ?all_instances:bool -> + ?raise_NoMatch:bool -> + ?upats_origin:ssrdir * constr -> + evar_map -> occ -> evar_map * tpattern list -> + find_P * conclude + +(** Example of [mk_tpattern_matcher] to implement + [rewrite \{occ\}\[in t\]rules]. + It first matches "in t" (called [pat]), then in all matched subterms + it matches the LHS of the rules using [find_R]. + [concl0] is the initial goal, [concl] will be the goal where some terms + are replaced by a De Bruijn index. The [rw_progress] extra check + selects only occurrences that are not rewritten to themselves (e.g. + an occurrence "x + x" rewritten with the commutativity law of addition + is skipped) {[ + let find_R, conclude = match pat with + | Some (_, In_T _) -> + let aux (sigma, pats) (d, r, lhs, rhs) = + let sigma, pat = + mk_tpattern env0 sigma0 (sigma, r) (rw_progress rhs) d lhs in + sigma, pats @ [pat] in + let rpats = List.fold_left aux (r_sigma, []) rules in + let find_R, end_R = mk_tpattern_matcher sigma0 occ rpats in + find_R ~k:(fun _ _ h -> mkRel h), + fun cl -> let rdx, d, r = end_R () in (d,r),rdx + | _ -> ... in + let concl = eval_pattern env0 sigma0 concl0 pat occ find_R in + let (d, r), rdx = conclude concl in ]} *) + +(* convenience shortcut: [pf_fill_occ_term gl occ (sigma,t)] returns + * the conclusion of [gl] where [occ] occurrences of [t] have been replaced + * by [Rel 1] and the instance of [t] *) +val pf_fill_occ_term : goal sigma -> occ -> evar_map * constr -> constr * constr + +(* It may be handy to inject a simple term into the first form of cpattern *) +val cpattern_of_term : char * glob_constr_and_expr -> cpattern + +(** Helpers to make stateful closures. Example: a [find_P] function may be + called many times, but the pattern instantiation phase is performed only the + first time. The corresponding [conclude] has to return the instantiated + pattern redex. Since it is up to [find_P] to raise [NoMatch] if the pattern + has no instance, [conclude] considers it an anomaly if the pattern did + not match *) + +(** [do_once r f] calls [f] and updates the ref only once *) +val do_once : 'a option ref -> (unit -> 'a) -> unit +(** [assert_done r] return the content of r. @raise Anomaly is r is [None] *) +val assert_done : 'a option ref -> 'a + +(** Very low level APIs. + these are calls to evarconv's [the_conv_x] followed by + [solve_unif_constraints_with_heuristics] and [resolve_typeclasses]. + In case of failure they raise [NoMatch] *) + +val unify_HO : env -> evar_map -> constr -> constr -> evar_map +val pf_unify_HO : goal sigma -> constr -> constr -> goal sigma + +(** Some more low level functions needed to implement the full SSR language + on top of the former APIs *) +val tag_of_cpattern : cpattern -> char +val loc_of_cpattern : cpattern -> Loc.t +val id_of_pattern : pattern -> Names.variable option +val is_wildcard : cpattern -> bool +val cpattern_of_id : Names.variable -> cpattern +val cpattern_of_id : Names.variable -> cpattern +val pr_constr_pat : constr -> Pp.std_ppcmds +val pf_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma +val pf_unsafe_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma + +(* One can also "Set SsrMatchingDebug" from a .v *) +val debug : bool -> unit + +(* One should delimit a snippet with "Set SsrMatchingProfiling" and + * "Unset SsrMatchingProfiling" to get timings *) +val profile : bool -> unit + +(* eof *) -- cgit v1.2.3