diff options
Diffstat (limited to 'plugins/ssrmatching/ssrmatching.ml4')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 683 |
1 files changed, 360 insertions, 323 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index d21223d4..307bc21a 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1,68 +1,55 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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) *) (************************************************************************) (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *) (* Defining grammar rules with "xx" in it automatically declares keywords too, * we thus save the lexer to restore it at the end of the file *) -let frozen_lexer = CLexer.freeze () ;; - -(*i camlp4use: "pa_extend.cmo" i*) -(*i camlp4deps: "grammar/grammar.cma" i*) +let frozen_lexer = CLexer.get_keyword_state () ;; +open Ltac_plugin open Names open Pp -open Pcoq open Genarg -open Constrarg +open Stdarg open Term +module CoqConstr = Constr +open CoqConstr +open Pcoq +open Pcoq.Constr open Vars -open Topconstr open Libnames open Tactics open Tacticals open Termops -open Namegen open Recordops open Tacmach -open Coqlib open Glob_term open Util open Evd -open Extend -open Goptions open Tacexpr -open Proofview.Notations open Tacinterp open Pretyping -open Constr -open Tactic -open Extraargs open Ppconstr open Printer - open Globnames open Misctypes open Decl_kinds open Evar_kinds open Constrexpr open Constrexpr_ops -open Notation_term -open Notation_ops -open Locus -open Locusops DECLARE PLUGIN "ssrmatching_plugin" -type loc = Loc.t -let dummy_loc = Loc.ghost -let errorstrm = CErrors.errorlabstrm "ssrmatching" -let loc_error loc msg = CErrors.user_err_loc (loc, msg, str msg) +let errorstrm = CErrors.user_err ~hdr:"ssrmatching" +let loc_error loc msg = CErrors.user_err ?loc ~hdr:msg (str msg) let ppnl = Feedback.msg_info (* 0 cost pp function. Active only if env variable SSRDEBUG is set *) @@ -76,27 +63,25 @@ let debug b = if b then pp_ref := ssr_pp else pp_ref := fun _ -> () let _ = Goptions.declare_bool_option - { Goptions.optsync = false; - Goptions.optname = "ssrmatching debugging"; + { Goptions.optname = "ssrmatching debugging"; Goptions.optkey = ["Debug";"SsrMatching"]; Goptions.optdepr = false; Goptions.optread = (fun _ -> !pp_ref == ssr_pp); Goptions.optwrite = debug } let pp s = !pp_ref s -(** Utils {{{ *****************************************************************) +(** Utils *)(* {{{ *****************************************************************) let env_size env = List.length (Environ.named_context env) let safeDestApp c = - match kind_of_term c with App (f, a) -> f, a | _ -> c, [| |] -let get_index = function ArgArg i -> i | _ -> - CErrors.anomaly (str"Uninterpreted index") + match kind c with App (f, a) -> f, a | _ -> c, [| |] (* Toplevel constr must be globalized twice ! *) -let glob_constr ist genv = function - | _, Some ce -> +let glob_constr ist genv sigma t = match t, ist with + | (_, Some ce), Some ist -> let vars = Id.Map.fold (fun x _ accu -> Id.Set.add x accu) ist.lfun Id.Set.empty in let ltacvars = { Constrintern.empty_ltac_sign with Constrintern.ltac_vars = vars } in - Constrintern.intern_gen WithoutTypeConstraint ~ltacvars:ltacvars genv ce - | rc, None -> rc + Constrintern.intern_gen WithoutTypeConstraint ~ltacvars:ltacvars genv sigma ce + | (rc, None), _ -> rc + | (_, Some _), None -> CErrors.anomaly Pp.(str"glob_constr: term with no ist") (* Term printing utilities functions for deciding bracketing. *) let pr_paren prx x = hov 1 (str "(" ++ prx x ++ str ")") @@ -115,7 +100,6 @@ let pr_guarded guard prc c = let s = Pp.string_of_ppcmds (prc c) ^ "$" in if guard s (skip_wschars s 0) then pr_paren prc c else prc c (* More sensible names for constr printers *) -let pr_constr = pr_constr let prl_glob_constr c = pr_lglob_constr_env (Global.env ()) c let pr_glob_constr c = pr_glob_constr_env (Global.env ()) c let prl_constr_expr = pr_lconstr_expr @@ -126,8 +110,8 @@ let prl_glob_constr_and_expr = function let pr_glob_constr_and_expr = function | _, Some c -> pr_constr_expr c | c, None -> pr_glob_constr c -let pr_term (k, c) = pr_guarded (guard_term k) pr_glob_constr_and_expr c -let prl_term (k, c) = pr_guarded (guard_term k) prl_glob_constr_and_expr c +let pr_term (k, c, _) = pr_guarded (guard_term k) pr_glob_constr_and_expr c +let prl_term (k, c, _) = pr_guarded (guard_term k) prl_glob_constr_and_expr c (** Adding a new uninterpreted generic argument type *) let add_genarg tag pr = @@ -147,39 +131,55 @@ let add_genarg tag pr = (** Constructors for cast type *) let dC t = CastConv t (** Constructors for constr_expr *) -let isCVar = function CRef (Ident _, _) -> true | _ -> false -let destCVar = function CRef (Ident (_, id), _) -> id | _ -> - CErrors.anomaly (str"not a CRef") -let mkCHole loc = CHole (loc, None, IntroAnonymous, None) -let mkCLambda loc name ty t = - CLambdaN (loc, [[loc, name], Default Explicit, ty], t) -let mkCLetIn loc name bo t = - CLetIn (loc, (loc, name), bo, t) -let mkCCast loc t ty = CCast (loc,t, dC ty) +let isCVar = function { CAst.v = CRef ({CAst.v=Ident _},_) } -> true | _ -> false +let destCVar = function { CAst.v = CRef ({CAst.v=Ident id},_) } -> id | _ -> + CErrors.anomaly (str"not a CRef.") +let isGLambda c = match DAst.get c with GLambda (Name _, _, _, _) -> true | _ -> false +let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c) + | _ -> CErrors.anomaly (str "not a GLambda") +let isGHole c = match DAst.get c with GHole _ -> true | _ -> false +let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) +let mkCLambda ?loc name ty t = CAst.make ?loc @@ + CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t) +let mkCLetIn ?loc name bo t = CAst.make ?loc @@ + CLetIn ((CAst.make ?loc name), bo, None, t) +let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty) (** Constructors for rawconstr *) -let mkRHole = GHole (dummy_loc, InternalHole, IntroAnonymous, None) -let mkRApp f args = if args = [] then f else GApp (dummy_loc, f, args) -let mkRCast rc rt = GCast (dummy_loc, rc, dC rt) -let mkRLambda n s t = GLambda (dummy_loc, n, Explicit, s, t) +let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None) +let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args) +let mkRCast rc rt = DAst.make @@ GCast (rc, dC rt) +let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t) (* ssrterm conbinators *) -let combineCG t1 t2 f g = match t1, t2 with - | (x, (t1, None)), (_, (t2, None)) -> x, (g t1 t2, None) - | (x, (_, Some t1)), (_, (_, Some t2)) -> x, (mkRHole, Some (f t1 t2)) - | _, (_, (_, None)) -> CErrors.anomaly (str"have: mixed C-G constr") - | _ -> CErrors.anomaly (str"have: mixed G-C constr") +let combineCG t1 t2 f g = + let mk_ist i1 i2 = match i1, i2 with + | None, Some i -> Some i + | Some i, None -> Some i + | None, None -> None + | Some i, Some j when i == j -> Some i + | _ -> CErrors.anomaly (Pp.str "combineCG: different ist") in + match t1, t2 with + | (x, (t1, None), i1), (_, (t2, None), i2) -> + x, (g t1 t2, None), mk_ist i1 i2 + | (x, (_, Some t1), i1), (_, (_, Some t2), i2) -> + x, (mkRHole, Some (f t1 t2)), mk_ist i1 i2 + | _, (_, (_, None), _) -> CErrors.anomaly (str"have: mixed C-G constr.") + | _ -> CErrors.anomaly (str"have: mixed G-C constr.") let loc_ofCG = function - | (_, (s, None)) -> Glob_ops.loc_of_glob_constr s - | (_, (_, Some s)) -> Constrexpr_ops.constr_loc s + | (_, (s, None), _) -> Glob_ops.loc_of_glob_constr s + | (_, (_, Some s), _) -> Constrexpr_ops.constr_loc s -let mk_term k c = k, (mkRHole, Some c) +let mk_term k c ist = k, (mkRHole, Some c), ist let mk_lterm = mk_term ' ' let pf_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl) sigma, ty +let nf_evar sigma c = + EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr c)) + (* }}} *) -(** Profiling {{{ *************************************************************) +(** Profiling *)(* {{{ *************************************************************) type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b; reset : unit -> unit; @@ -195,8 +195,7 @@ let profile b = ;; let _ = Goptions.declare_bool_option - { Goptions.optsync = false; - Goptions.optname = "ssrmatching profiling"; + { Goptions.optname = "ssrmatching profiling"; Goptions.optkey = ["SsrMatchingProfiling"]; Goptions.optread = (fun _ -> !profile_now); Goptions.optdepr = false; @@ -297,14 +296,15 @@ let unif_EQ_args env sigma pa a = prof_unif_eq_args.profile (unif_EQ_args env sigma pa) a ;; -let unif_HO env ise p c = Evarconv.the_conv_x env p c ise - -let unif_HOtype env ise p c = Evarconv.the_conv_x_leq env p c ise +let unif_HO env ise p c = + try Evarconv.the_conv_x env p c ise + with Evarconv.UnableToUnify(ise, err) -> + raise Pretype_errors.(PretypeError(env,ise,CannotUnify(p,c,Some err))) let unif_HO_args env ise0 pa i ca = let n = Array.length pa in let rec loop ise j = - if j = n then ise else loop (unif_HO env ise pa.(j) ca.(i + j)) (j + 1) in + if j = n then ise else loop (unif_HO env ise (EConstr.of_constr pa.(j)) (EConstr.of_constr ca.(i + j))) (j + 1) in loop ise0 0 (* FO unification should boil down to calling w_unify with no_delta, but *) @@ -331,12 +331,13 @@ let flags_FO = (Unification.default_no_delta_unify_flags ()).Unification.resolve_evars } let unif_FO env ise p c = - Unification.w_unify env ise Reduction.CONV ~flags:flags_FO p c + Unification.w_unify env ise Reduction.CONV ~flags:flags_FO (EConstr.of_constr p) (EConstr.of_constr c) (* Perform evar substitution in main term and prune substitution. *) let nf_open_term sigma0 ise c = + let c = EConstr.Unsafe.to_constr c in let s = ise and s' = ref sigma0 in - let rec nf c' = match kind_of_term c' with + let rec nf c' = match kind c' with | Evar ex -> begin try nf (existential_value s ex) with _ -> let k, a = ex in let a' = Array.map nf a in @@ -344,14 +345,14 @@ let nf_open_term sigma0 ise c = s' := Evd.add !s' k (Evarutil.nf_evar_info s (Evd.find s k)); mkEvar (k, a') end - | _ -> map_constr nf c' in + | _ -> map nf c' in let copy_def k evi () = if evar_body evi != Evd.Evar_empty then () else match Evd.evar_body (Evd.find s k) with | Evar_defined c' -> s' := Evd.define k (nf c') !s' | _ -> () in let c' = nf c in let _ = Evd.fold copy_def sigma0 () in - !s', Evd.evar_universe_context s, c' + !s', Evd.evar_universe_context s, EConstr.of_constr c' let unif_end env sigma0 ise0 pt ok = let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in @@ -363,12 +364,7 @@ let unif_end env sigma0 ise0 pt ok = if ise2 == ise1 then (s, uc, t) else let s, uc', t = nf_open_term sigma0 ise2 t in - s, Evd.union_evar_universe_context uc uc', t - -let pf_unif_HO gl sigma pt p c = - let env = pf_env gl in - let ise = unif_HO env (create_evar_defs sigma) p c in - unif_end env (project gl) ise pt (fun _ -> true) + s, UState.union uc uc', t let unify_HO env sigma0 t1 t2 = let sigma = unif_HO env sigma0 t1 t2 in @@ -381,7 +377,7 @@ let pf_unify_HO gl t1 t2 = re_sig si sigma (* This is what the definition of iter_constr should be... *) -let iter_constr_LR f c = match kind_of_term c with +let iter_constr_LR f c = match kind c with | Evar (k, a) -> Array.iter f a | Cast (cc, _, t) -> f cc; f t | Prod (_, t, b) | Lambda (_, t, b) -> f t; f b @@ -412,12 +408,12 @@ let inv_dir = function L2R -> R2L | R2L -> L2R type pattern_class = | KpatFixed | KpatConst - | KpatEvar of existential_key + | KpatEvar of Evar.t | KpatLet | KpatLam | KpatRigid | KpatFlex - | KpatProj of constant + | KpatProj of Constant.t type tpattern = { up_k : pattern_class; @@ -426,7 +422,7 @@ type tpattern = { up_a : constr array; up_t : constr; (* equation proof term or matched term *) up_dir : ssrdir; (* direction of the rule *) - up_ok : constr -> evar_map -> bool; (* progess test for rewrite *) + up_ok : constr -> evar_map -> bool; (* progress test for rewrite *) } let all_ok _ _ = true @@ -434,32 +430,27 @@ let all_ok _ _ = true let proj_nparams c = try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0 -let isFixed c = match kind_of_term c with - | Var _ | Ind _ | Construct _ | Const _ | Proj _ -> true - | _ -> false - -let isRigid c = match kind_of_term c with +let isRigid c = match kind c with | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true | _ -> false -exception UndefPat - -let hole_var = mkVar (id_of_string "_") +let hole_var = mkVar (Id.of_string "_") let pr_constr_pat c0 = let rec wipe_evar c = - if isEvar c then hole_var else map_constr wipe_evar c in - pr_constr (wipe_evar c0) + if isEvar c then hole_var else map wipe_evar c in + let sigma, env = Pfedit.get_current_context () in + pr_constr_env env sigma (wipe_evar c0) (* Turn (new) evars into metas *) let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = let ise = ref ise0 in let sigma = ref ise0 in let nenv = env_size env + if hack then 1 else 0 in - let rec put c = match kind_of_term c with + let rec put c = match kind c with | Evar (k, a as ex) -> begin try put (existential_value !sigma ex) with NotInstantiatedEvar -> - if Evd.mem sigma0 k then map_constr put c else + if Evd.mem sigma0 k then map put c else let evi = Evd.find !sigma k in let dc = List.firstn (max 0 (Array.length a - nenv)) (evar_filtered_context evi) in let abs_dc (d, c) = function @@ -471,28 +462,30 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = Context.Named.fold_inside abs_dc ~init:([], (put evi.evar_concl)) dc in let m = Evarutil.new_meta () in ise := meta_declare m t !ise; - sigma := Evd.define k (applist (mkMeta m, a)) !sigma; + sigma := Evd.define k (applistc (mkMeta m) a) !sigma; put (existential_value !sigma ex) end - | _ -> map_constr put c in + | _ -> map put c in let c1 = put c0 in !ise, c1 (* Compile a match pattern from a term; t is the term to fill. *) (* p_origin can be passed to obtain a better error message *) let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = let k, f, a = - let f, a = Reductionops.whd_betaiota_stack ise p in - match kind_of_term f with + let f, a = Reductionops.whd_betaiota_stack ise (EConstr.of_constr p) in + let f = EConstr.Unsafe.to_constr f in + let a = List.map EConstr.Unsafe.to_constr a in + match kind f with | Const (p,_) -> let np = proj_nparams p in if np = 0 || np > List.length a then KpatConst, f, a else - let a1, a2 = List.chop np a in KpatProj p, applist(f, a1), a2 + let a1, a2 = List.chop np a in KpatProj p, (applistc f a1), a2 | Proj (p,arg) -> KpatProj (Projection.constant p), f, a | 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 - (match p_origin with None -> CErrors.error "indeterminate pattern" + (match p_origin with None -> CErrors.user_err Pp.(str "indeterminate pattern") | Some (dir, rule) -> errorstrm (str "indeterminate " ++ pr_dir_side dir ++ str " in " ++ pr_constr_pat rule)) @@ -510,7 +503,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = (* kind and arity for Proj and Flex patterns. *) let ungen_upat lhs (sigma, uc, t) u = let f, a = safeDestApp lhs in - let k = match kind_of_term f with + let k = match kind f with | Var _ | Ind _ | Construct _ -> KpatFixed | Const _ -> KpatConst | Evar (k, _) -> if is_defined sigma k then raise NoMatch else KpatEvar k @@ -522,37 +515,37 @@ let ungen_upat lhs (sigma, uc, t) u = let nb_cs_proj_args pc f u = let na k = List.length (snd (lookup_canonical_conversion (ConstRef pc, k))).o_TCOMPS in - try match kind_of_term f with - | Prod _ -> na Prod_cs - | Sort s -> na (Sort_cs (family_of_sort s)) - | Const (c',_) when Constant.equal c' pc -> - begin match kind_of_term u.up_f with + let nargs_of_proj t = match kind t with | App(_,args) -> Array.length args | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be the number of arguments including the projected *) - | _ -> assert false - end + | _ -> assert false in + 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 + | 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 with Not_found -> -1 let isEvar_k k f = - match kind_of_term f with Evar (k', _) -> k = k' | _ -> false + match kind f with Evar (k', _) -> k = k' | _ -> false let nb_args c = - match kind_of_term c with App (_, a) -> Array.length a | _ -> 0 + match kind c with App (_, a) -> Array.length a | _ -> 0 let mkSubArg i a = if i = Array.length a then a else Array.sub a 0 i let mkSubApp f i a = if i = 0 then f else mkApp (f, mkSubArg i a) let splay_app ise = - let rec loop c a = match kind_of_term c with + let rec loop c a = match kind c with | App (f, a') -> loop f (Array.append a' a) | Cast (c', _, _) -> loop c' a | Evar ex -> (try loop (existential_value ise ex) a with _ -> c, a) | _ -> c, a in - fun c -> match kind_of_term c with + fun c -> match kind c with | App (f, a) -> loop f a | Cast _ | Evar _ -> loop c [| |] | _ -> c, [| |] @@ -561,8 +554,8 @@ let filter_upat i0 f n u fpats = let na = Array.length u.up_a in if n < na then fpats else let np = match u.up_k with - | KpatConst when Term.eq_constr u.up_f f -> na - | KpatFixed when Term.eq_constr u.up_f f -> na + | KpatConst when eq_constr_nounivs u.up_f f -> na + | KpatFixed when eq_constr_nounivs u.up_f f -> na | KpatEvar k when isEvar_k k f -> na | KpatLet when isLetIn f -> na | KpatLam when isLambda f -> na @@ -574,7 +567,7 @@ let filter_upat i0 f n u fpats = if np < na then fpats else let () = if !i0 < np then i0 := n in (u, np) :: fpats -let eq_prim_proj c t = match kind_of_term t with +let eq_prim_proj c t = match kind t with | Proj(p,_) -> Constant.equal (Projection.constant p) c | _ -> false @@ -582,17 +575,17 @@ let filter_upat_FO i0 f n u fpats = let np = nb_args u.up_FO in if n < np then fpats else let ok = match u.up_k with - | KpatConst -> Term.eq_constr u.up_f f - | KpatFixed -> Term.eq_constr u.up_f f + | KpatConst -> eq_constr_nounivs u.up_f f + | KpatFixed -> eq_constr_nounivs u.up_f f | KpatEvar k -> isEvar_k k f | KpatLet -> isLetIn f | KpatLam -> isLambda f | KpatRigid -> isRigid f - | KpatProj pc -> Term.eq_constr f (mkConst pc) || eq_prim_proj pc f + | KpatProj pc -> equal f (mkConst pc) || eq_prim_proj pc f | KpatFlex -> i0 := n; true in if ok then begin if !i0 < np then i0 := np; (u, np) :: fpats end else fpats -exception FoundUnif of (evar_map * evar_universe_context * tpattern) +exception FoundUnif of (evar_map * UState.t * tpattern) (* Note: we don't update env as we descend into the term, as the primitive *) (* unification procedure always rejects subterms with bound variables. *) @@ -638,17 +631,18 @@ let match_upats_FO upats env sigma0 ise orig_c = | _ -> unif_FO env ise u.up_FO c' in let ise' = (* Unify again using HO to assign evars *) let p = mkApp (u.up_f, u.up_a) in - try unif_HO env ise p c' with _ -> raise NoMatch in + try unif_HO env ise (EConstr.of_constr p) (EConstr.of_constr c') with e when CErrors.noncritical e -> raise NoMatch in let lhs = mkSubApp f i a in - let pt' = unif_end env sigma0 ise' u.up_t (u.up_ok lhs) in + let pt' = unif_end env sigma0 ise' (EConstr.of_constr u.up_t) (u.up_ok lhs) in + let pt' = pi1 pt', pi2 pt', EConstr.Unsafe.to_constr (pi3 pt') in raise (FoundUnif (ungen_upat lhs pt' u)) with FoundUnif (s,_,_) as sig_u when dont_impact_evars s -> raise sig_u - | Not_found -> CErrors.anomaly (str"incomplete ise in match_upats_FO") - | _ -> () in + | Not_found -> CErrors.anomaly (str"incomplete ise in match_upats_FO.") + | e when CErrors.noncritical e -> () in List.iter one_match fpats done; iter_constr_LR loop f; Array.iter loop a in - try loop orig_c with Invalid_argument _ -> CErrors.anomaly (str"IN FO") + try loop orig_c with Invalid_argument _ -> CErrors.anomaly (str"IN FO.") let prof_FO = mk_profiler "match_upats_FO";; let match_upats_FO upats env sigma0 ise c = @@ -657,7 +651,7 @@ let match_upats_FO upats env sigma0 ise c = let match_upats_HO ~on_instance upats env sigma0 ise c = - let dont_impact_evars = dont_impact_evars_in c in + let dont_impact_evars = dont_impact_evars_in c in let it_did_match = ref false in let failed_because_of_TC = ref false in let rec aux upats env sigma0 ise c = @@ -679,16 +673,17 @@ let match_upats_HO ~on_instance upats env sigma0 ise c = | KpatLet -> let x, v, t, b = destLetIn f in let _, pv, _, pb = destLetIn u.up_f in - let ise' = unif_HO env ise pv v in + let ise' = unif_HO env ise (EConstr.of_constr pv) (EConstr.of_constr v) in unif_HO (Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, t)) env) - ise' pb b + ise' (EConstr.of_constr pb) (EConstr.of_constr b) | KpatFlex | KpatProj _ -> - unif_HO env ise u.up_f (mkSubApp f (i - Array.length u.up_a) a) - | _ -> unif_HO env ise u.up_f f in + unif_HO env ise (EConstr.of_constr u.up_f) (EConstr.of_constr(mkSubApp f (i - Array.length u.up_a) a)) + | _ -> unif_HO env ise (EConstr.of_constr u.up_f) (EConstr.of_constr f) in let ise'' = unif_HO_args env ise' u.up_a (i - Array.length u.up_a) a in let lhs = mkSubApp f i a in - let pt' = unif_end env sigma0 ise'' u.up_t (u.up_ok lhs) in + let pt' = unif_end env sigma0 ise'' (EConstr.of_constr u.up_t) (u.up_ok lhs) in + let pt' = pi1 pt', pi2 pt', EConstr.Unsafe.to_constr (pi3 pt') in on_instance (ungen_upat lhs pt' u) with FoundUnif (s,_,_) as sig_u when dont_impact_evars s -> raise sig_u | NoProgress -> it_did_match := true @@ -713,27 +708,27 @@ let match_upats_HO ~on_instance upats env sigma0 ise c = let fixed_upat = function | {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false -| {up_t = t} -> not (occur_existential t) +| {up_t = t} -> not (occur_existential Evd.empty (EConstr.of_constr t)) (** FIXME *) let do_once r f = match !r with Some _ -> () | None -> r := Some (f ()) let assert_done r = - match !r with Some x -> x | None -> CErrors.anomaly (str"do_once never called") + match !r with Some x -> x | None -> CErrors.anomaly (str"do_once never called.") let assert_done_multires r = match !r with - | None -> CErrors.anomaly (str"do_once never called") + | None -> CErrors.anomaly (str"do_once never called.") | Some (n, xs) -> r := Some (n+1,xs); try List.nth xs n with Failure _ -> raise NoMatch -type subst = Environ.env -> Term.constr -> Term.constr -> int -> Term.constr +type subst = Environ.env -> constr -> constr -> int -> constr type find_P = - Environ.env -> Term.constr -> int -> + Environ.env -> constr -> int -> k:subst -> - Term.constr + constr type conclude = unit -> - Term.constr * ssrdir * (Evd.evar_map * Evd.evar_universe_context * Term.constr) + constr * ssrdir * (Evd.evar_map * UState.t * constr) (* upats_origin makes a better error message only *) let mk_tpattern_matcher ?(all_instances=false) @@ -759,13 +754,13 @@ let mk_tpattern_matcher ?(all_instances=false) let x, pv, t, pb = destLetIn u.up_f in let env' = Environ.push_rel (Context.Rel.Declaration.LocalAssum(x, t)) env in - let match_let f = match kind_of_term f with + let match_let f = match kind f with | LetIn (_, v, _, b) -> unif_EQ env sigma pv v && unif_EQ env' sigma pb b | _ -> false in match_let - | KpatFixed -> Term.eq_constr u.up_f - | KpatConst -> Term.eq_constr u.up_f + | KpatFixed -> eq_constr_nounivs u.up_f + | KpatConst -> eq_constr_nounivs u.up_f | KpatLam -> fun c -> - (match kind_of_term c with + (match kind c with | Lambda _ -> unif_EQ env sigma u.up_f c | _ -> false) | _ -> unif_EQ env sigma u.up_f in @@ -779,7 +774,7 @@ let source () = match upats_origin, upats with | Some (dir,rule), _ -> str"The " ++ pr_dir_side dir ++ str" of " ++ pr_constr_pat rule ++ spc() | _, [] | None, _::_::_ -> - CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin") in + CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin.") in let on_instance, instances = let instances = ref [] in (fun x -> @@ -789,15 +784,15 @@ let on_instance, instances = let rec uniquize = function | [] -> [] | (sigma,_,{ up_f = f; up_a = a; up_t = t } as x) :: xs -> - let t = Reductionops.nf_evar sigma t in - let f = Reductionops.nf_evar sigma f in - let a = Array.map (Reductionops.nf_evar sigma) a in + let t = nf_evar sigma t in + let f = nf_evar sigma f in + let a = Array.map (nf_evar sigma) a in let neq (sigma1,_,{ up_f = f1; up_a = a1; up_t = t1 }) = - let t1 = Reductionops.nf_evar sigma1 t1 in - let f1 = Reductionops.nf_evar sigma1 f1 in - let a1 = Array.map (Reductionops.nf_evar sigma1) a1 in - not (Term.eq_constr t t1 && - Term.eq_constr f f1 && CArray.for_all2 Term.eq_constr a a1) in + let t1 = nf_evar sigma1 t1 in + let f1 = nf_evar sigma1 f1 in + let a1 = Array.map (nf_evar sigma1) a1 in + not (equal t t1 && + equal f f1 && CArray.for_all2 equal a a1) in x :: uniquize (List.filter neq xs) in ((fun env c h ~k -> @@ -817,7 +812,7 @@ let rec uniquize = function errorstrm (source () ++ str "does not match any subterm of the goal") | NoProgress when (not raise_NoMatch) -> let dir = match upats_origin with Some (d,_) -> d | _ -> - CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin") in + CErrors.anomaly (str"mk_tpattern_matcher with no upats_origin.") in errorstrm (str"all matches of "++source()++ str"are equal to the " ++ pr_dir_side (inv_dir dir)) | NoProgress -> raise NoMatch); @@ -844,15 +839,18 @@ let rec uniquize = function | Context.Rel.Declaration.LocalAssum _ as x -> x | Context.Rel.Declaration.LocalDef (x,_,y) -> Context.Rel.Declaration.LocalAssum(x,y) in - Environ.push_rel ctx_item env, h' + 1 in - let f' = map_constr_with_binders_left_to_right inc_h subst_loop acc f in + EConstr.push_rel ctx_item env, h' + 1 in + let self acc c = EConstr.of_constr (subst_loop acc (EConstr.Unsafe.to_constr c)) in + let f = EConstr.of_constr f in + let f' = map_constr_with_binders_left_to_right sigma inc_h self acc f in + let f' = EConstr.Unsafe.to_constr f' in mkApp (f', Array.map_left (subst_loop acc) a) in subst_loop (env,h) c) : find_P), ((fun () -> let sigma, uc, ({up_f = pf; up_a = pa} as u) = match !upat_that_matched with | Some (_,x) -> List.hd x | None when raise_NoMatch -> raise NoMatch - | None -> CErrors.anomaly (str"companion function never called") in + | None -> CErrors.anomaly (str"companion function never called.") in let p' = mkApp (pf, pa) in if max_occ <= !nocc then p', u.up_dir, (sigma, uc, u.up_t) else errorstrm (str"Only " ++ int !nocc ++ str" < " ++ int max_occ ++ @@ -900,23 +898,16 @@ let pr_pattern_aux pr_constr = function | E_As_X_In_T (e,x,t) -> pr_constr e ++ str " as " ++ pr_constr x ++ str " in " ++ pr_constr t let pp_pattern (sigma, p) = - pr_pattern_aux (fun t -> pr_constr_pat (pi3 (nf_open_term sigma sigma t))) p + pr_pattern_aux (fun t -> pr_constr_pat (EConstr.Unsafe.to_constr (pi3 (nf_open_term sigma sigma (EConstr.of_constr t))))) p let pr_cpattern = pr_term let pr_rpattern _ _ _ = pr_pattern -let pr_option f = function None -> mt() | Some x -> f x -let pr_ssrpattern _ _ _ = pr_option pr_pattern -let pr_pattern_squarep = pr_option (fun r -> str "[" ++ pr_pattern r ++ str "]") -let pr_ssrpattern_squarep _ _ _ = pr_pattern_squarep -let pr_pattern_roundp = pr_option (fun r -> str "(" ++ pr_pattern r ++ str ")") -let pr_ssrpattern_roundp _ _ _ = pr_pattern_roundp - let wit_rpatternty = add_genarg "rpatternty" pr_pattern let glob_ssrterm gs = function - | k, (_, Some c) -> k, + | k, (_, Some c), None -> let x = Tacintern.intern_constr gs c in - fst x, Some c + k, (fst x, Some c), None | ct -> ct (* This piece of code asserts the following notations are reserved *) @@ -926,33 +917,33 @@ let glob_ssrterm gs = function (* Reserved Notation "( a 'as' b 'in' c )" (at level 0). *) let glob_cpattern gs p = pp(lazy(str"globbing pattern: " ++ pr_term p)); - let glob x = snd (glob_ssrterm gs (mk_lterm x)) in + let glob x = pi2 (glob_ssrterm gs (mk_lterm x None)) in let encode k s l = - let name = Name (id_of_string ("_ssrpat_" ^ s)) in - k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None) in + let name = Name (Id.of_string ("_ssrpat_" ^ s)) in + k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None), None in let bind_in t1 t2 = - let d = dummy_loc in let n = Name (destCVar t1) in - fst (glob (mkCCast d (mkCHole d) (mkCLambda d n (mkCHole d) t2))) in + let mkCHole = mkCHole ~loc:None in let n = Name (destCVar t1) in + fst (glob (mkCCast mkCHole (mkCLambda n mkCHole t2))) in let check_var t2 = if not (isCVar t2) then loc_error (constr_loc t2) "Only identifiers are allowed here" in match p with - | _, (_, None) as x -> x - | k, (v, Some t) as orig -> - if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else - match t with - | CNotation(_, "( _ in _ )", ([t1; t2], [], [])) -> + | _, (_, None), _ as x -> x + | k, (v, Some t), _ as orig -> + if k = 'x' then glob_ssrterm gs ('(', (v, Some t), None) else + match t.CAst.v with + | CNotation("( _ in _ )", ([t1; t2], [], [], [])) -> (try match glob t1, glob t2 with | (r1, None), (r2, None) -> encode k "In" [r1;r2] | (r1, Some _), (r2, Some _) when isCVar t1 -> encode k "In" [r1; r2; bind_in t1 t2] | (r1, Some _), (r2, Some _) -> encode k "In" [r1; r2] - | _ -> CErrors.anomaly (str"where are we?") + | _ -> CErrors.anomaly (str"where are we?.") with _ when isCVar t1 -> encode k "In" [bind_in t1 t2]) - | CNotation(_, "( _ in _ in _ )", ([t1; t2; t3], [], [])) -> + | CNotation("( _ in _ in _ )", ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "In" [fst (glob t1); bind_in t2 t3] - | CNotation(_, "( _ as _ )", ([t1; t2], [], [])) -> + | CNotation("( _ as _ )", ([t1; t2], [], [], [])) -> encode k "As" [fst (glob t1); fst (glob t2)] - | CNotation(_, "( _ as _ in _ )", ([t1; t2; t3], [], [])) -> + | CNotation("( _ as _ in _ )", ([t1; t2; t3], [], [], [])) -> check_var t2; encode k "As" [fst (glob t1); bind_in t2 t3] | _ -> glob_ssrterm gs orig ;; @@ -966,7 +957,8 @@ let glob_rpattern s p = | E_In_X_In_T(e,x,t) -> E_In_X_In_T (glob_ssrterm s e,x,glob_ssrterm s t) | E_As_X_In_T(e,x,t) -> E_As_X_In_T (glob_ssrterm s e,x,glob_ssrterm s t) -let subst_ssrterm s (k, c) = k, Tacsubst.subst_glob_constr_and_expr s c +let subst_ssrterm s (k, c, ist) = + k, Tacsubst.subst_glob_constr_and_expr s c, ist let subst_rpattern s = function | T t -> T (subst_ssrterm s t) @@ -976,41 +968,56 @@ let subst_rpattern s = function | E_In_X_In_T(e,x,t) -> E_In_X_In_T (subst_ssrterm s e,x,subst_ssrterm s t) | E_As_X_In_T(e,x,t) -> E_As_X_In_T (subst_ssrterm s e,x,subst_ssrterm s t) +let interp_ssrterm ist (k,t,_) = k, t, Some ist + +let interp_rpattern s = function + | T t -> T (interp_ssrterm s t) + | In_T t -> In_T (interp_ssrterm s t) + | X_In_T(x,t) -> X_In_T (interp_ssrterm s x,interp_ssrterm s t) + | In_X_In_T(x,t) -> In_X_In_T (interp_ssrterm s x,interp_ssrterm s t) + | E_In_X_In_T(e,x,t) -> + E_In_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t) + | E_As_X_In_T(e,x,t) -> + E_As_X_In_T (interp_ssrterm s e,interp_ssrterm s x,interp_ssrterm s t) + +let interp_rpattern ist gl t = Tacmach.project gl, interp_rpattern ist t + ARGUMENT EXTEND rpattern TYPED AS rpatternty PRINTED BY pr_rpattern + INTERPRETED BY interp_rpattern GLOBALIZED BY glob_rpattern SUBSTITUTED BY subst_rpattern - | [ lconstr(c) ] -> [ T (mk_lterm c) ] - | [ "in" lconstr(c) ] -> [ In_T (mk_lterm c) ] + | [ lconstr(c) ] -> [ T (mk_lterm c None) ] + | [ "in" lconstr(c) ] -> [ In_T (mk_lterm c None) ] | [ lconstr(x) "in" lconstr(c) ] -> - [ X_In_T (mk_lterm x, mk_lterm c) ] + [ X_In_T (mk_lterm x None, mk_lterm c None) ] | [ "in" lconstr(x) "in" lconstr(c) ] -> - [ In_X_In_T (mk_lterm x, mk_lterm c) ] + [ In_X_In_T (mk_lterm x None, mk_lterm c None) ] | [ lconstr(e) "in" lconstr(x) "in" lconstr(c) ] -> - [ E_In_X_In_T (mk_lterm e, mk_lterm x, mk_lterm c) ] + [ E_In_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None) ] | [ lconstr(e) "as" lconstr(x) "in" lconstr(c) ] -> - [ E_As_X_In_T (mk_lterm e, mk_lterm x, mk_lterm c) ] + [ E_As_X_In_T (mk_lterm e None, mk_lterm x None, mk_lterm c None) ] END -type cpattern = char * glob_constr_and_expr -let tag_of_cpattern = fst +type cpattern = char * glob_constr_and_expr * Geninterp.interp_sign option +let tag_of_cpattern = pi1 let loc_of_cpattern = loc_ofCG -let cpattern_of_term t = t +let cpattern_of_term (c, t) ist = c, t, Some ist type occ = (bool * int list) option type rpattern = (cpattern, cpattern) ssrpattern -let pr_rpattern = pr_pattern -type pattern = Evd.evar_map * (Term.constr, Term.constr) ssrpattern +type pattern = Evd.evar_map * (constr, constr) ssrpattern - -let id_of_cpattern = function - | _,(_,Some (CRef (Ident (_, x), _))) -> Some x - | _,(_,Some (CAppExpl (_, (_, Ident (_, x), _), []))) -> Some x - | _,(GRef (_, VarRef x, _) ,None) -> Some x +let id_of_cpattern (_, (c1, c2), _) = + let open CAst in + match DAst.get c1, c2 with + | _, Some { v = CRef ({CAst.v=Ident x}, _) } -> Some x + | _, Some { v = CAppExpl ((_, {CAst.v=Ident x}, _), []) } -> Some x + | GRef (VarRef x, _), None -> Some x | _ -> None let id_of_Cterm t = match id_of_cpattern t with | Some x -> x @@ -1032,19 +1039,17 @@ let interp_wit wit ist gl x = let arg = interp_genarg ist globarg in let (sigma, arg) = of_ftactic arg gl in sigma, Value.cast (topwit wit) arg -let interp_constr = interp_wit wit_constr let interp_open_constr ist gl gc = interp_wit wit_open_constr ist gl gc -let pf_intern_term ist gl (_, c) = glob_constr ist (pf_env gl) c -let interp_term ist gl (_, c) = (interp_open_constr ist gl c) +let pf_intern_term gl (_, c, ist) = glob_constr ist (pf_env gl) (project gl) c let pr_ssrterm _ _ _ = pr_term -let input_ssrtermkind strm = match Compat.get_tok (stream_nth 0 strm) with +let input_ssrtermkind strm = match stream_nth 0 strm with | Tok.KEYWORD "(" -> '(' | Tok.KEYWORD "@" -> '@' | _ -> ' ' -let ssrtermkind = Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind +let ssrtermkind = Pcoq.Gram.Entry.of_parser "ssrtermkind" input_ssrtermkind -let interp_ssrterm _ gl t = Tacmach.project gl, t +let interp_ssrterm ist gl t = Tacmach.project gl, interp_ssrterm ist t ARGUMENT EXTEND cpattern PRINTED BY pr_ssrterm @@ -1052,16 +1057,16 @@ ARGUMENT EXTEND cpattern GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm RAW_PRINTED BY pr_ssrterm GLOB_PRINTED BY pr_ssrterm -| [ "Qed" constr(c) ] -> [ mk_lterm c ] +| [ "Qed" constr(c) ] -> [ mk_lterm c None ] END -let (!@) = Compat.to_coqloc - GEXTEND Gram GLOBAL: cpattern; cpattern: [[ k = ssrtermkind; c = constr -> - let pattern = mk_term k c in - if loc_ofCG pattern <> !@loc && k = '(' then mk_term 'x' c else pattern ]]; + let pattern = mk_term k c None in + if loc_ofCG pattern <> Some !@loc && k = '(' + then mk_term 'x' c None + else pattern ]]; END ARGUMENT EXTEND lcpattern @@ -1071,16 +1076,23 @@ ARGUMENT EXTEND lcpattern GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm RAW_PRINTED BY pr_ssrterm GLOB_PRINTED BY pr_ssrterm -| [ "Qed" lconstr(c) ] -> [ mk_lterm c ] +| [ "Qed" lconstr(c) ] -> [ mk_lterm c None ] END GEXTEND Gram GLOBAL: lcpattern; lcpattern: [[ k = ssrtermkind; c = lconstr -> - let pattern = mk_term k c in - if loc_ofCG pattern <> !@loc && k = '(' then mk_term 'x' c else pattern ]]; + let pattern = mk_term k c None in + if loc_ofCG pattern <> Some !@loc && k = '(' + then mk_term 'x' c None + else pattern ]]; END +let interp_term gl = function + | (_, c, Some ist) -> + on_snd EConstr.Unsafe.to_constr (interp_open_constr ist gl c) + | _ -> errorstrm (str"interpreting a term with no ist") + let thin id sigma goal = let ids = Id.Set.singleton id in let env = Goal.V82.env sigma goal in @@ -1098,33 +1110,38 @@ let thin id sigma goal = let sigma = Goal.V82.partial_solution_to sigma goal gl ev in sigma +(* let pr_ist { lfun= lfun } = prlist_with_sep spc (fun (id, Geninterp.Val.Dyn(ty,_)) -> pr_id id ++ str":" ++ Geninterp.Val.pr ty) (Id.Map.bindings lfun) +*) -let interp_pattern ?wit_ssrpatternarg ist gl red redty = +let interp_pattern ?wit_ssrpatternarg gl red redty = pp(lazy(str"interpreting: " ++ pr_pattern red)); - pp(lazy(str" in ist: " ++ pr_ist ist)); let xInT x y = X_In_T(x,y) and inXInT x y = In_X_In_T(x,y) in let inT x = In_T x and eInXInT e x t = E_In_X_In_T(e,x,t) in let eAsXInT e x t = E_As_X_In_T(e,x,t) in - let mkG ?(k=' ') x = k,(x,None) in - let decode ist t ?reccall f g = - try match (pf_intern_term ist gl t) with - | GCast(_,GHole _,CastConv(GLambda(_,Name x,_,_,c))) -> f x (' ',(c,None)) - | GVar(_,id) - when Id.Map.mem id ist.lfun && + let mkG ?(k=' ') x ist = k,(x,None), ist in + let ist_of (_,_,ist) = ist in + let decode (_,_,ist as t) ?reccall f g = + try match DAst.get (pf_intern_term gl t) with + | GCast(t,CastConv c) when isGHole t && isGLambda c-> + let (x, c) = destGLambda c in + f x (' ',(c,None),ist) + | GVar id + when Option.has_some ist && let ist = Option.get ist in + Id.Map.mem id ist.lfun && not(Option.is_empty reccall) && not(Option.is_empty wit_ssrpatternarg) -> - let v = Id.Map.find id ist.lfun in + let v = Id.Map.find id (Option.get ist).lfun in Option.get reccall (Value.cast (topwit (Option.get wit_ssrpatternarg)) v) | it -> g t with e when CErrors.noncritical e -> g t in - let decodeG t f g = decode ist (mkG t) f g in - let bad_enc id _ = CErrors.anomaly (str"bad encoding for pattern "++str id) in + let decodeG ist t f g = decode (mkG t ist) f g in + let bad_enc id _ = CErrors.anomaly (str"bad encoding for pattern "++str id++str".") in let cleanup_XinE h x rp sigma = - let h_k = match kind_of_term h with Evar (k,_) -> k | _ -> assert false in + let h_k = match kind h with Evar (k,_) -> k | _ -> assert false in let to_clean, update = (* handle rename if x is already used *) let ctx = pf_hyps gl in let len = Context.Named.length ctx in @@ -1139,12 +1156,12 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = with Not_found -> ref (Some x), fun _ -> () in let sigma0 = project gl in let new_evars = - let rec aux acc t = match kind_of_term t with + let rec aux acc t = match kind t with | Evar (k,_) -> if k = h_k || List.mem k acc || Evd.mem sigma0 k then acc else (update k; k::acc) - | _ -> fold_constr aux acc t in - aux [] (Evarutil.nf_evar sigma rp) in + | _ -> CoqConstr.fold aux acc t in + aux [] (nf_evar sigma rp) in let sigma = List.fold_left (fun sigma e -> if Evd.is_defined sigma e then sigma else (* clear may be recursive *) @@ -1154,71 +1171,82 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = thin name sigma e) sigma new_evars in sigma in - let red = let rec decode_red (ist,red) = match red with - | T(k,(GCast (_,GHole _,(CastConv(GLambda (_,Name id,_,_,t)))),None)) - when let id = string_of_id id in let len = String.length id in + let red = let rec decode_red = function + | T(k,(t,None),ist) -> + begin match DAst.get t with + | GCast (c,CastConv t) + when isGHole c && + let (id, t) = destGLambda t in + let id = Id.to_string id in let len = String.length id in (len > 8 && String.sub id 0 8 = "_ssrpat_") -> - let id = string_of_id id in let len = String.length id in - (match String.sub id 8 (len - 8), t with - | "In", GApp(_, _, [t]) -> decodeG t xInT (fun x -> T x) - | "In", GApp(_, _, [e; t]) -> decodeG t (eInXInT (mkG e)) (bad_enc id) - | "In", GApp(_, _, [e; t; e_in_t]) -> - decodeG t (eInXInT (mkG e)) - (fun _ -> decodeG e_in_t xInT (fun _ -> assert false)) - | "As", GApp(_, _, [e; t]) -> decodeG t (eAsXInT (mkG e)) (bad_enc id) + let (id, t) = destGLambda t in + let id = Id.to_string id in let len = String.length id in + (match String.sub id 8 (len - 8), DAst.get t with + | "In", GApp( _, [t]) -> decodeG ist t xInT (fun x -> T x) + | "In", GApp( _, [e; t]) -> decodeG ist t (eInXInT (mkG e ist)) (bad_enc id) + | "In", GApp( _, [e; t; e_in_t]) -> + decodeG ist t (eInXInT (mkG e ist)) + (fun _ -> decodeG ist e_in_t xInT (fun _ -> assert false)) + | "As", GApp(_, [e; t]) -> decodeG ist t (eAsXInT (mkG e ist)) (bad_enc id) | _ -> bad_enc id ()) - | T t -> decode ist ~reccall:decode_red t xInT (fun x -> T x) - | In_T t -> decode ist t inXInT inT - | X_In_T (e,t) -> decode ist t (eInXInT e) (fun x -> xInT (id_of_Cterm e) x) + | _ -> + decode ~reccall:decode_red (mkG ~k t ist) xInT (fun x -> T x) + end + | T t -> decode ~reccall:decode_red t xInT (fun x -> T x) + | In_T t -> decode t inXInT inT + | X_In_T (e,t) -> decode t (eInXInT e) (fun x -> xInT (id_of_Cterm e) x) | In_X_In_T (e,t) -> inXInT (id_of_Cterm e) t | E_In_X_In_T (e,x,rp) -> eInXInT e (id_of_Cterm x) rp | E_As_X_In_T (e,x,rp) -> eAsXInT e (id_of_Cterm x) rp in - decode_red (ist,red) in + decode_red red in pp(lazy(str"decoded as: " ++ pr_pattern_w_ids red)); - let red = match redty with None -> red | Some ty -> let ty = ' ', ty in + let red = + match redty with + | None -> red + | Some (ty, ist) -> let ty = ' ', ty, Some ist in match red with - | T t -> T (combineCG t ty (mkCCast (loc_ofCG t)) mkRCast) + | T t -> T (combineCG t ty (mkCCast ?loc:(loc_ofCG t)) mkRCast) | X_In_T (x,t) -> - let ty = pf_intern_term ist gl ty in - E_As_X_In_T (mkG (mkRCast mkRHole ty), x, t) + let gty = pf_intern_term gl ty in + E_As_X_In_T (mkG (mkRCast mkRHole gty) (ist_of ty), x, t) | E_In_X_In_T (e,x,t) -> - let ty = mkG (pf_intern_term ist gl ty) in - E_In_X_In_T (combineCG e ty (mkCCast (loc_ofCG t)) mkRCast, x, t) + let ty = mkG (pf_intern_term gl ty) (ist_of ty) in + E_In_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t) | E_As_X_In_T (e,x,t) -> - let ty = mkG (pf_intern_term ist gl ty) in - E_As_X_In_T (combineCG e ty (mkCCast (loc_ofCG t)) mkRCast, x, t) + let ty = mkG (pf_intern_term gl ty) (ist_of ty) in + E_As_X_In_T (combineCG e ty (mkCCast ?loc:(loc_ofCG t)) mkRCast, x, t) | red -> red in pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); - let mkXLetIn loc x (a,(g,c)) = match c with - | Some b -> a,(g,Some (mkCLetIn loc x (mkCHole loc) b)) - | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), g), None) in + let mkXLetIn ?loc x (a,(g,c),ist) = match c with + | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b)), ist + | None -> a,(DAst.make ?loc @@ GLetIn (x, DAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None), ist in match red with - | T t -> let sigma, t = interp_term ist gl t in sigma, T t - | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t + | T t -> let sigma, t = interp_term gl t in sigma, T t + | In_T t -> let sigma, t = interp_term gl t in sigma, In_T t | X_In_T (x, rp) | In_X_In_T (x, rp) -> let mk x p = match red with X_In_T _ -> X_In_T(x,p) | _ -> In_X_In_T(x,p) in - let rp = mkXLetIn dummy_loc (Name x) rp in - let sigma, rp = interp_term ist gl rp in + let rp = mkXLetIn (Name x) rp in + let sigma, rp = interp_term gl rp in let _, h, _, rp = destLetIn rp in let sigma = cleanup_XinE h x rp sigma in - let rp = subst1 h (Evarutil.nf_evar sigma rp) in + let rp = subst1 h (nf_evar sigma rp) in sigma, mk h rp | E_In_X_In_T(e, x, rp) | E_As_X_In_T (e, x, rp) -> let mk e x p = match red with E_In_X_In_T _ ->E_In_X_In_T(e,x,p)|_->E_As_X_In_T(e,x,p) in - let rp = mkXLetIn dummy_loc (Name x) rp in - let sigma, rp = interp_term ist gl rp in + let rp = mkXLetIn (Name x) rp in + let sigma, rp = interp_term gl rp in let _, h, _, rp = destLetIn rp in let sigma = cleanup_XinE h x rp sigma in - let rp = subst1 h (Evarutil.nf_evar sigma rp) in - let sigma, e = interp_term ist (re_sig (sig_it gl) sigma) e in + let rp = subst1 h (nf_evar sigma rp) in + let sigma, e = interp_term (re_sig (sig_it gl) sigma) e in sigma, mk e h rp ;; -let interp_cpattern ist gl red redty = interp_pattern ist gl (T red) redty;; -let interp_rpattern ~wit_ssrpatternarg ist gl red = interp_pattern ~wit_ssrpatternarg ist gl red None;; +let interp_cpattern gl red redty = interp_pattern gl (T red) redty;; +let interp_rpattern ~wit_ssrpatternarg gl red = interp_pattern ~wit_ssrpatternarg gl red None;; let id_of_pattern = function - | _, T t -> (match kind_of_term t with Var id -> Some id | _ -> None) + | _, T t -> (match kind t with Var id -> Some id | _ -> None) | _ -> None (* The full occurrence set *) @@ -1226,11 +1254,11 @@ let noindex = Some(false,[]) (* calls do_subst on every sub-term identified by (pattern,occ) *) let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = - let fs sigma x = Reductionops.nf_evar sigma x in + let fs sigma x = nf_evar sigma x in let pop_evar sigma e p = let { Evd.evar_body = e_body } as e_def = Evd.find sigma e in let e_body = match e_body with Evar_defined c -> c - | _ -> errorstrm (str "Matching the pattern " ++ pr_constr p ++ + | _ -> errorstrm (str "Matching the pattern " ++ pr_constr_env env0 sigma0 p ++ str " did not instantiate ?" ++ int (Evar.repr e) ++ spc () ++ str "Does the variable bound by the \"in\" construct occur "++ str "in the pattern?") in @@ -1238,21 +1266,21 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = Evd.add (Evd.remove sigma e) e {e_def with Evd.evar_body = Evar_empty} in sigma, e_body in let ex_value hole = - match kind_of_term hole with Evar (e,_) -> e | _ -> assert false in + match kind hole with Evar (e,_) -> e | _ -> assert false in let mk_upat_for ?hack env sigma0 (sigma, t) ?(p=t) ok = let sigma,pat= mk_tpattern ?hack env sigma0 (sigma,p) ok L2R (fs sigma t) in sigma, [pat] in match pattern with - | None -> do_subst env0 concl0 concl0 1 + | None -> do_subst env0 concl0 concl0 1, UState.empty | 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 let rp = mk_upat_for env0 sigma0 (ise, rp) all_ok in let find_T, end_T = mk_tpattern_matcher ?raise_NoMatch sigma0 occ rp in - let concl = find_T env0 concl0 1 do_subst in - let _ = end_T () in - concl + let concl = find_T env0 concl0 1 ~k:do_subst in + let _, _, (_, us, _) = end_T () in + concl, us | Some (sigma, (X_In_T (hole, p) | In_X_In_T (hole, p))) -> let p = fs sigma p in let occ = match pattern with Some (_, X_In_T _) -> occ | _ -> noindex in @@ -1262,13 +1290,13 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = (* we start from sigma, so hole is considered a rigid head *) let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in let find_X, end_X = mk_tpattern_matcher ?raise_NoMatch sigma occ holep in - let concl = find_T env0 concl0 1 (fun env c _ h -> - let p_sigma = unify_HO env (create_evar_defs sigma) c p in + 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 - (fun env _ -> do_subst env e_body))) in - let _ = end_X () in let _ = end_T () in - concl + ~k:(fun env _ -> do_subst env e_body))) in + let _ = end_X () in let _, _, (_, us, _) = end_T () in + concl, us | Some (sigma, E_In_X_In_T (e, hole, p)) -> let p, e = fs sigma p, fs sigma e in let ex = ex_value hole in @@ -1278,42 +1306,43 @@ let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = let find_X, end_X = mk_tpattern_matcher sigma noindex holep in let re = mk_upat_for env0 sigma0 (sigma, e) all_ok in let find_E, end_E = mk_tpattern_matcher ?raise_NoMatch sigma0 occ re in - let concl = find_T env0 concl0 1 (fun env c _ h -> - let p_sigma = unify_HO env (create_evar_defs sigma) c p in + 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 (fun env c _ h -> - find_E env e_body h do_subst))) in - let _ = end_E () in let _ = end_X () in let _ = end_T () in - concl + fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h -> + find_E env e_body h ~k:do_subst))) in + let _,_,(_,us,_) = end_E () in + let _ = end_X () in let _ = end_T () in + concl, us | 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 e_sigma = unify_HO env0 sigma hole e in + 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 let find_TE, end_TE = mk_tpattern_matcher sigma0 noindex rp in let holep = mk_upat_for env0 sigma (sigma, hole) all_ok in let find_X, end_X = mk_tpattern_matcher sigma occ holep in - let concl = find_TE env0 concl0 1 (fun env c _ h -> - let p_sigma = unify_HO env (create_evar_defs sigma) c p in + let concl = find_TE 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 (fun env c _ h -> - let e_sigma = unify_HO env sigma e_body e in + fs p_sigma (find_X env (fs sigma p) h ~k:(fun env c _ h -> + let e_sigma = unify_HO env sigma (EConstr.of_constr e_body) (EConstr.of_constr e) in let e_body = fs e_sigma e in do_subst env e_body e_body h))) in - let _ = end_X () in let _ = end_TE () in - concl + let _ = end_X () in let _,_,(_,us,_) = end_TE () in + concl, us ;; let redex_of_pattern ?(resolve_typeclasses=false) env (sigma, p) = let e = match p with - | In_T _ | In_X_In_T _ -> CErrors.anomaly (str"pattern without redex") + | In_T _ | In_X_In_T _ -> CErrors.anomaly (str"pattern without redex.") | T e | X_In_T (e, _) | E_As_X_In_T (e, _, _) | E_In_X_In_T (e, _, _) -> e in let sigma = if not resolve_typeclasses then sigma else Typeclasses.resolve_typeclasses ~fail:false env sigma in - Reductionops.nf_evar sigma e, Evd.evar_universe_context sigma + nf_evar sigma e, Evd.evar_universe_context sigma let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h = let do_make_rel, occ = @@ -1321,12 +1350,14 @@ let fill_occ_pattern ?raise_NoMatch env sigma cl pat occ h = let find_R, conclude = let r = ref None in (fun env c _ h' -> - do_once r (fun () -> c, Evd.empty_evar_universe_context); + do_once r (fun () -> c); if do_make_rel then mkRel (h'+h-1) else c), - (fun _ -> if !r = None then redex_of_pattern env pat else assert_done r) in - let cl = eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in + (fun _ -> if !r = None then fst(redex_of_pattern env pat) + else assert_done r) in + let cl, us = + eval_pattern ?raise_NoMatch env sigma cl (Some pat) occ find_R in let e = conclude cl in - e, cl + (e, us), cl ;; (* clenup interface for external use *) @@ -1334,19 +1365,25 @@ let mk_tpattern ?p_origin env sigma0 sigma_t f dir c = mk_tpattern ?p_origin env sigma0 sigma_t f dir c ;; +let eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst = + fst (eval_pattern ?raise_NoMatch env0 sigma0 concl0 pattern occ do_subst) +;; + let pf_fill_occ env concl occ sigma0 p (sigma, t) ok h = + let p = EConstr.Unsafe.to_constr p in + let concl = EConstr.Unsafe.to_constr concl in let ise = create_evar_defs sigma in - let ise, u = mk_tpattern env sigma0 (ise,t) ok L2R p in + let ise, u = mk_tpattern env sigma0 (ise,EConstr.Unsafe.to_constr t) ok L2R p in let find_U, end_U = mk_tpattern_matcher ~raise_NoMatch:true sigma0 occ (ise,[u]) in - let concl = find_U env concl h (fun _ _ _ -> mkRel) in + let concl = find_U env concl h ~k:(fun _ _ _ -> mkRel) in let rdx, _, (sigma, uc, p) = end_U () in - sigma, uc, p, concl, rdx + sigma, uc, EConstr.of_constr p, EConstr.of_constr concl, EConstr.of_constr rdx let fill_occ_term env cl occ sigma0 (sigma, t) = try let sigma',uc,t',cl,_= pf_fill_occ env cl occ sigma0 t (sigma, t) all_ok 1 in - if sigma' != sigma0 then CErrors.error "matching impacts evars" + if sigma' != sigma0 then CErrors.user_err Pp.(str "matching impacts evars") else cl, (Evd.merge_universe_context sigma' uc, t') with NoMatch -> try let sigma', uc, t' = @@ -1354,7 +1391,7 @@ let fill_occ_term env cl occ sigma0 (sigma, t) = if sigma' != sigma0 then raise NoMatch else cl, (Evd.merge_universe_context sigma' uc, t') with _ -> - errorstrm (str "partial term " ++ pr_constr_pat t + errorstrm (str "partial term " ++ pr_constr_pat (EConstr.Unsafe.to_constr t) ++ str " does not match any subterm of the goal") let pf_fill_occ_term gl occ t = @@ -1362,25 +1399,20 @@ let pf_fill_occ_term gl occ t = let cl,(_,t) = fill_occ_term env concl occ sigma0 t in cl, t -let cpattern_of_id id = ' ', (GRef (dummy_loc, VarRef id, None), None) +let cpattern_of_id id = + ' ', (DAst.make @@ GRef (VarRef id, None), None), Some Geninterp.({ lfun = Id.Map.empty; extra = Tacinterp.TacStore.empty }) -let is_wildcard = function - | _,(_,Some (CHole _)|GHole _,None) -> true +let is_wildcard ((_, (l, r), _) : cpattern) : bool = match DAst.get l, r with + | _, Some { CAst.v = CHole _ } | GHole _, None -> true | _ -> false (* "ssrpattern" *) -let pr_ssrpatternarg _ _ _ (_,cpat) = pr_rpattern cpat -let pr_ssrpatternarg_glob _ _ _ cpat = pr_rpattern cpat -let interp_ssrpatternarg ist gl p = project gl, (ist, p) -ARGUMENT EXTEND ssrpatternarg - PRINTED BY pr_ssrpatternarg - INTERPRETED BY interp_ssrpatternarg - GLOBALIZED BY glob_rpattern - RAW_PRINTED BY pr_ssrpatternarg_glob - GLOB_PRINTED BY pr_ssrpatternarg_glob +ARGUMENT EXTEND ssrpatternarg TYPED AS rpattern PRINTED BY pr_rpattern | [ rpattern(pat) ] -> [ pat ] END + +let pr_rpattern = pr_pattern let pf_merge_uc uc gl = re_sig (sig_it gl) (Evd.merge_universe_context (project gl) uc) @@ -1388,16 +1420,19 @@ let pf_merge_uc uc gl = let pf_unsafe_merge_uc uc gl = re_sig (sig_it gl) (Evd.set_universe_context (project gl) uc) -let interp_rpattern ist gl red = interp_rpattern ~wit_ssrpatternarg ist gl red +let interp_rpattern = interp_rpattern ~wit_ssrpatternarg -let ssrpatterntac _ist (arg_ist,arg) gl = - let pat = interp_rpattern arg_ist gl arg in +let ssrpatterntac _ist arg gl = + let pat = interp_rpattern gl arg in let sigma0 = project gl in let concl0 = pf_concl gl in + let concl0 = EConstr.Unsafe.to_constr concl0 in let (t, uc), concl_x = fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in + let t = EConstr.of_constr t in + let concl_x = EConstr.of_constr concl_x in let gl, tty = pf_type_of gl t in - let concl = mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in + let concl = EConstr.mkLetIn (Name (Id.of_string "selected"), t, tty, concl_x) in Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl (* Register "ssrpattern" tactic *) @@ -1410,23 +1445,25 @@ let () = let name = { mltac_plugin = "ssrmatching_plugin"; mltac_tactic = "ssrpattern"; } in let () = Tacenv.register_ml_tactic name [|mltac|] in let tac = - TacFun ([Some (Id.of_string "pattern")], - TacML (Loc.ghost, { mltac_name = name; mltac_index = 0 }, [])) in + TacFun ([Name (Id.of_string "pattern")], + TacML (Loc.tag ({ mltac_name = name; mltac_index = 0 }, []))) in let obj () = Tacenv.register_ltac true false (Id.of_string "ssrpattern") tac in Mltop.declare_cache_obj obj "ssrmatching_plugin" -let ssrinstancesof ist arg gl = +let ssrinstancesof arg gl = let ok rhs lhs ise = true in -(* not (Term.eq_constr lhs (Evarutil.nf_evar ise rhs)) in *) +(* not (equal lhs (Evarutil.nf_evar ise rhs)) in *) let env, sigma, concl = pf_env gl, project gl, pf_concl gl in - let sigma0, cpat = interp_cpattern ist gl arg None in + let concl = EConstr.Unsafe.to_constr concl in + let sigma0, cpat = interp_cpattern gl arg None in let pat = match cpat with T x -> x | _ -> errorstrm (str"Not supported") in let etpat, tpat = mk_tpattern env sigma (sigma0,pat) (ok pat) L2R pat in let find, conclude = mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma None (etpat,[tpat]) in - let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr p ++ spc() ++ str "matches:" ++ spc() ++ pr_constr c)); c in + let print env p c _ = ppnl (hov 1 (str"instance:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) p ++ spc() + ++ str "matches:" ++ spc() ++ pr_constr_env (pf_env gl) (gl.sigma) c)); c in ppnl (str"BEGIN INSTANCES"); try while true do @@ -1435,13 +1472,13 @@ let ssrinstancesof ist arg gl = with NoMatch -> ppnl (str"END INSTANCES"); tclIDTAC gl TACTIC EXTEND ssrinstoftpat -| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof ist arg) ] +| [ "ssrinstancesoftpat" cpattern(arg) ] -> [ Proofview.V82.tactic (ssrinstancesof arg) ] END (* We wipe out all the keywords generated by the grammar rules we defined. *) (* The user is supposed to Require Import ssreflect or Require ssreflect *) (* and Import ssreflect.SsrSyntax to obtain these keywords and as a *) (* consequence the extended ssreflect grammar. *) -let () = CLexer.unfreeze frozen_lexer ;; +let () = CLexer.set_keyword_state frozen_lexer ;; (* vim: set filetype=ocaml foldmethod=marker: *) |