diff options
Diffstat (limited to 'debian/patches/0005-ssrmatching-license.patch')
| -rw-r--r-- | debian/patches/0005-ssrmatching-license.patch | 298 |
1 files changed, 298 insertions, 0 deletions
diff --git a/debian/patches/0005-ssrmatching-license.patch b/debian/patches/0005-ssrmatching-license.patch new file mode 100644 index 00000000..f207cc8b --- /dev/null +++ b/debian/patches/0005-ssrmatching-license.patch @@ -0,0 +1,298 @@ +From: Benjamin Barenblat <bbaren@debian.org> +Subject: Replace deleted non-free ssrmatching files with free ones +Forwarded: not-needed +Last-Update: 2019-01-17 + +Coq 8.8.2 shipped with two files in ssrmatching that were licensed under +CeCILL-B, which I believe is a nonfree license. I've removed them from +the Debian source package (see gbp.conf). This patch replaces them with +equivalent files (from a later version) that are licensed freely. + +These files are present starting at upstream commit +f613d9f9f0c8aec814272f6c2dcdce7e70da47b6. I've modified them by where required +to get them to compile against 8.8.2. +--- /dev/null ++++ b/plugins/ssrmatching/ssrmatching.mli +@@ -0,0 +1,242 @@ ++(************************************************************************) ++(* * The Coq Proof Assistant / The Coq Development Team *) ++(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) ++(* <O___,, * (see CREDITS file for the list of authors) *) ++(* \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) *) ++(************************************************************************) ++ ++(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) ++ ++open Goal ++open Environ ++open Evd ++open Constr ++open Genintern ++ ++(** ******** 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.t ++ ++(** 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.t ++ ++(** 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.t ++ ++(** 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 : ++ 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 : ++ goal sigma -> ++ cpattern -> (Tacexpr.glob_constr_and_expr * Geninterp.interp_sign) 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.t ++ ++(** 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 * UState.t * 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 * EConstr.t -> EConstr.t * EConstr.t ++ ++(* It may be handy to inject a simple term into the first form of cpattern *) ++val cpattern_of_term : char * Tacexpr.glob_constr_and_expr -> Geninterp.interp_sign -> 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]. ++ In case of failure they raise [NoMatch] *) ++ ++val unify_HO : env -> evar_map -> EConstr.constr -> EConstr.constr -> evar_map ++val pf_unify_HO : goal sigma -> EConstr.constr -> EConstr.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 option ++val id_of_pattern : pattern -> Names.Id.t option ++val is_wildcard : cpattern -> bool ++val cpattern_of_id : Names.Id.t -> cpattern ++val pr_constr_pat : constr -> Pp.t ++val pf_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma ++val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma ++ ++(* One can also "Set SsrMatchingDebug" from a .v *) ++val debug : bool -> unit ++ ++val ssrinstancesof : cpattern -> Tacmach.tactic ++ ++val profile : bool -> unit ++val wit_cpattern : cpattern Genarg.uniform_genarg_type ++val lcpattern : cpattern Pcoq.Gram.entry ++val wit_lcpattern : cpattern Genarg.uniform_genarg_type ++val cpattern : cpattern Pcoq.Gram.entry ++val wit_rpattern : rpattern Genarg.uniform_genarg_type ++val rpattern : rpattern Pcoq.Gram.entry ++ ++(* eof *) +--- /dev/null ++++ b/plugins/ssrmatching/ssrmatching.v +@@ -0,0 +1,37 @@ ++(************************************************************************) ++(* * The Coq Proof Assistant / The Coq Development Team *) ++(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) ++(* <O___,, * (see CREDITS file for the list of authors) *) ++(* \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) *) ++(************************************************************************) ++ ++(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) ++ ++Declare ML Module "ssrmatching_plugin". ++ ++Module SsrMatchingSyntax. ++ ++(* Reserve the notation for rewrite patterns so that the user is not allowed *) ++(* to declare it at a different level. *) ++Reserved Notation "( a 'in' b )" (at level 0). ++Reserved Notation "( a 'as' b )" (at level 0). ++Reserved Notation "( a 'in' b 'in' c )" (at level 0). ++Reserved Notation "( a 'as' b 'in' c )" (at level 0). ++ ++Delimit Scope ssrpatternscope with pattern. ++ ++(* Notation to define shortcuts for the "X in t" part of a pattern. *) ++Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope. ++ ++(* Some shortcuts for recurrent "X in t" parts. *) ++Notation RHS := (X in _ = X)%pattern. ++Notation LHS := (X in X = _)%pattern. ++ ++End SsrMatchingSyntax. ++ ++Export SsrMatchingSyntax. ++ ++Tactic Notation "ssrpattern" ssrpatternarg(p) := ssrpattern p . |