diff options
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 62 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.mli | 52 |
2 files changed, 57 insertions, 57 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 9682487a22..6cb464918a 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -310,7 +310,7 @@ let pf_unify_HO gl t1 t2 = (* This is what the definition of iter_constr should be... *) let iter_constr_LR f c = match kind c with | Evar (k, a) -> Array.iter f a - | Cast (cc, _, t) -> f cc; f t + | Cast (cc, _, t) -> f cc; f t | Prod (_, t, b) | Lambda (_, t, b) -> f t; f b | LetIn (_, v, t, b) -> f v; f t; f b | App (cf, a) -> f cf; Array.iter f a @@ -423,10 +423,10 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = | Var _ | Ind _ | Construct _ -> KpatFixed, f, a | Evar (k, _) -> if Evd.mem sigma0 k then KpatEvar k, f, a else - if a <> [] then KpatFlex, f, a else + if a <> [] then KpatFlex, f, a else (match p_origin with None -> CErrors.user_err Pp.(str "indeterminate pattern") | Some (dir, rule) -> - errorstrm (str "indeterminate " ++ pr_dir_side dir + errorstrm (str "indeterminate " ++ pr_dir_side dir ++ str " in " ++ pr_constr_pat env ise rule)) | LetIn (_, v, _, b) -> if b <> mkRel 1 then KpatLet, f, a else KpatFlex, v, a @@ -435,7 +435,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = let aa = Array.of_list a in let ise', p' = evars_for_FO ~hack env sigma0 ise (mkApp (f, aa)) in ise', - { up_k = k; up_FO = p'; up_f = f; + { up_k = k; up_FO = p'; up_f = f; up_a = aa; up_ok = ok; up_dir = dir; up_t = t} (* Specialize a pattern after a successful match: assign a precise head *) @@ -462,7 +462,7 @@ let nb_cs_proj_args pc f u = try match kind f with | Prod _ -> na Prod_cs | Sort s -> na (Sort_cs (Sorts.family s)) - | Const (c',_) when Constant.equal c' pc -> nargs_of_proj u.up_f + | Const (c',_) when Constant.equal c' pc -> nargs_of_proj u.up_f | Proj (c',_) when Constant.equal (Projection.constant c') pc -> nargs_of_proj u.up_f | Var _ | Ind _ | Construct _ | Const _ -> na (Const_cs (global_of_constr f)) | _ -> -1 @@ -636,15 +636,15 @@ let match_upats_HO ~on_instance upats env sigma0 ise c = let fixed_upat evd = function -| {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false +| {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false | {up_t = t} -> not (occur_existential evd (EConstr.of_constr t)) (** FIXME *) let do_once r f = match !r with Some _ -> () | None -> r := Some (f ()) -let assert_done r = +let assert_done r = match !r with Some x -> x | None -> CErrors.anomaly (str"do_once never called.") -let assert_done_multires r = +let assert_done_multires r = match !r with | None -> CErrors.anomaly (str"do_once never called.") | Some (e, n, xs) -> @@ -652,7 +652,7 @@ let assert_done_multires r = try List.nth xs n with Failure _ -> raise NoMatch type subst = Environ.env -> constr -> constr -> int -> constr -type find_P = +type find_P = Environ.env -> constr -> int -> k:subst -> constr @@ -677,7 +677,7 @@ let mk_tpattern_matcher ?(all_instances=false) if !nocc = max_occ then skip_occ := use_occ; if !nocc <= max_occ then occ_set.(!nocc - 1) else not use_occ in let upat_that_matched = ref None in - let match_EQ env sigma u = + let match_EQ env sigma u = match u.up_k with | KpatLet -> let x, pv, t, pb = destLetIn u.up_f in @@ -693,14 +693,14 @@ let mk_tpattern_matcher ?(all_instances=false) | Lambda _ -> unif_EQ env sigma u.up_f c | _ -> false) | _ -> unif_EQ env sigma u.up_f in -let p2t p = mkApp(p.up_f,p.up_a) in +let p2t p = mkApp(p.up_f,p.up_a) in let source env = match upats_origin, upats with - | None, [p] -> + | None, [p] -> (if fixed_upat ise p then str"term " else str"partial term ") ++ pr_constr_pat env ise (p2t p) ++ spc() - | Some (dir,rule), [p] -> str"The " ++ pr_dir_side dir ++ str" of " ++ + | Some (dir,rule), [p] -> str"The " ++ pr_dir_side dir ++ str" of " ++ pr_constr_pat env ise rule ++ fnl() ++ ws 4 ++ pr_constr_pat env ise (p2t p) ++ fnl() - | Some (dir,rule), _ -> str"The " ++ pr_dir_side dir ++ str" of " ++ + | Some (dir,rule), _ -> str"The " ++ pr_dir_side dir ++ str" of " ++ pr_constr_pat env ise rule ++ spc() | _, [] | None, _::_::_ -> CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin.") in @@ -724,8 +724,8 @@ let rec uniquize = function equal f f1 && CArray.for_all2 equal a a1) in x :: uniquize (List.filter neq xs) in -((fun env c h ~k -> - do_once upat_that_matched (fun () -> +((fun env c h ~k -> + do_once upat_that_matched (fun () -> let failed_because_of_TC = ref false in try if not all_instances then match_upats_FO upats env sigma0 ise c; @@ -789,14 +789,14 @@ let rec uniquize = function ws 4 ++ pr_constr_pat env sigma p' ++ fnl () ++ str"of " ++ pr_constr_pat env sigma rule)) : conclude) -type ('ident, 'term) ssrpattern = +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 - + | 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 + let pr_pattern = function | T t -> prl_term t | In_T t -> str "in " ++ prl_term t @@ -944,7 +944,7 @@ let of_ftactic ftac gl = in (sigma, ans) -let interp_wit wit ist gl x = +let interp_wit wit ist gl x = let globarg = in_gen (glbwit wit) x in let arg = interp_genarg ist globarg in let (sigma, arg) = of_ftactic arg gl in @@ -1026,9 +1026,9 @@ let interp_pattern ?wit_ssrpatternarg gl red redty = | Evar (k,_) -> if k = h_k || List.mem k acc || Evd.mem sigma0 k then acc else (update k; k::acc) - | _ -> CoqConstr.fold aux acc t in + | _ -> CoqConstr.fold aux acc t in aux [] (nf_evar sigma rp) in - let sigma = + let sigma = List.fold_left (fun sigma e -> if Evd.is_defined sigma e then sigma else (* clear may be recursive *) if Option.is_empty !to_clean then sigma else @@ -1128,7 +1128,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = str " did not instantiate ?" ++ int (Evar.repr e) ++ spc () ++ str "Does the variable bound by the \"in\" construct occur "++ str "in the pattern?") in - let sigma = + let sigma = Evd.add (Evd.remove sigma e) e {e_def with Evd.evar_body = Evar_empty} in sigma, e_body in let ex_value hole = @@ -1138,7 +1138,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = sigma, [pat] in match pattern with | None -> do_subst env0 concl0 concl0 1, UState.empty - | Some (sigma, (T rp | In_T rp)) -> + | Some (sigma, (T rp | In_T rp)) -> let rp = fs sigma rp in let ise = create_evar_defs sigma in let occ = match pattern with Some (_, T _) -> occ | _ -> noindex in @@ -1159,7 +1159,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let concl = find_T env0 concl0 1 ~k:(fun env c _ h -> let p_sigma = unify_HO env (create_evar_defs sigma) (EConstr.of_constr c) (EConstr.of_constr p) in let sigma, e_body = pop_evar p_sigma ex p in - fs p_sigma (find_X env (fs sigma p) h + fs p_sigma (find_X env (fs sigma p) h ~k:(fun env _ -> do_subst env e_body))) in let _ = end_X () in let _, _, (_, us, _) = end_T () in concl, us @@ -1183,7 +1183,7 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = | Some (sigma, E_As_X_In_T (e, hole, p)) -> let p, e = fs sigma p, fs sigma e in let ex = ex_value hole in - let rp = + let rp = let e_sigma = unify_HO env0 sigma (EConstr.of_constr hole) (EConstr.of_constr e) in e_sigma, fs e_sigma p in let rp = mk_upat_for ~hack:true env0 sigma0 rp all_ok in @@ -1227,7 +1227,7 @@ let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h = ;; (* clenup interface for external use *) -let mk_tpattern ?p_origin env sigma0 sigma_t f dir c = +let mk_tpattern ?p_origin env sigma0 sigma_t f dir c = mk_tpattern ?p_origin env sigma0 sigma_t f dir c ;; @@ -1275,7 +1275,7 @@ let is_wildcard ((_, (l, r), _) : cpattern) : bool = match DAst.get l, r with (* "ssrpattern" *) let pr_rpattern = pr_pattern - + let pf_merge_uc uc gl = re_sig (sig_it gl) (Evd.merge_universe_context (project gl) uc) diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index c6b85738ec..b6ccb4cc6e 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -20,7 +20,7 @@ open Genintern (** Pattern parsing *) -(** The type of context patterns, the patterns of the [set] tactic and +(** 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 @@ -78,10 +78,10 @@ type occ = (bool * int list) option 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 + [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]. + [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] *) @@ -91,12 +91,12 @@ val eval_pattern : 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]) +(** [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 : @@ -107,7 +107,7 @@ val fill_occ_pattern : (** *************************** Low level APIs ****************************** *) -(* The primitive matching facility. It matches of a term with holes, like +(* 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 @@ -116,7 +116,7 @@ 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] +(** [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. @@ -130,14 +130,14 @@ val mk_tpattern : 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 +(** [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 + [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 = @@ -150,11 +150,11 @@ type find_P = type conclude = unit -> constr * ssrdir * (evar_map * UState.t * constr) -(** [mk_tpattern_matcher b o sigma0 occ sigma_tplist] creates a pair +(** [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 + 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 -> @@ -163,24 +163,24 @@ val mk_tpattern_matcher : evar_map -> occ -> evar_map * tpattern list -> find_P * conclude -(** Example of [mk_tpattern_matcher] to implement +(** 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 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 + 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 = + 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), + 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 @@ -194,7 +194,7 @@ val pf_fill_occ_term : goal sigma -> occ -> evar_map * EConstr.t -> EConstr.t * (* It may be handy to inject a simple term into the first form of cpattern *) val cpattern_of_term : char * glob_constr_and_expr -> Geninterp.interp_sign -> cpattern -(** Helpers to make stateful closures. Example: a [find_P] function may be +(** 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 |