From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 6 Nov 2017 23:27:09 +0100 Subject: [api] Move structures deprecated in the API to the core. We do up to `Term` which is the main bulk of the changes. --- plugins/ssrmatching/ssrmatching.ml4 | 81 +++++++++++++++++++------------------ plugins/ssrmatching/ssrmatching.mli | 2 +- 2 files changed, 42 insertions(+), 41 deletions(-) (limited to 'plugins/ssrmatching') diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index e3e34616b..d5c9e4988 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -18,10 +18,13 @@ let frozen_lexer = CLexer.get_keyword_state () ;; open Ltac_plugin open Names open Pp -open Pcoq open Genarg open Stdarg open Term +module CoqConstr = Constr +open CoqConstr +open Pcoq +open Pcoq.Constr open Vars open Libnames open Tactics @@ -35,10 +38,8 @@ open Evd open Tacexpr open Tacinterp open Pretyping -open Constr open Ppconstr open Printer - open Globnames open Misctypes open Decl_kinds @@ -73,7 +74,7 @@ let pp s = !pp_ref s (** 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, [| |] + match kind c with App (f, a) -> f, a | _ -> c, [| |] (* Toplevel constr must be globalized twice ! *) let glob_constr ist genv = function | _, Some ce -> @@ -325,7 +326,7 @@ let unif_FO env ise p c = 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 @@ -333,7 +334,7 @@ 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 @@ -365,7 +366,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 @@ -418,14 +419,14 @@ let all_ok _ _ = true let proj_nparams c = try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0 -let isRigid c = match kind_of_term c with +let isRigid c = match kind c with | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true | _ -> false 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 + if isEvar c then hole_var else map wipe_evar c in pr_constr (wipe_evar c0) (* Turn (new) evars into metas *) @@ -433,11 +434,11 @@ 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 @@ -452,7 +453,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = 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. *) @@ -462,7 +463,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = 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_of_term f with + match kind f with | Const (p,_) -> let np = proj_nparams p in if np = 0 || np > List.length a then KpatConst, f, a else @@ -490,7 +491,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 @@ -502,14 +503,14 @@ 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 - let nargs_of_proj t = match kind_of_term t 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 in - try match kind_of_term f with + try match kind f with | Prod _ -> na Prod_cs - | Sort s -> na (Sort_cs (family_of_sort s)) + | 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)) @@ -517,22 +518,22 @@ let nb_cs_proj_args pc f u = 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, [| |] @@ -541,8 +542,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 equal u.up_f f -> na + | KpatFixed when equal u.up_f f -> na | KpatEvar k when isEvar_k k f -> na | KpatLet when isLetIn f -> na | KpatLam when isLambda f -> na @@ -554,7 +555,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 @@ -562,13 +563,13 @@ 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 -> equal u.up_f f + | KpatFixed -> equal 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 @@ -741,13 +742,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 -> equal u.up_f + | KpatConst -> equal 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 @@ -778,8 +779,8 @@ let rec uniquize = function let t1 = nf_evar sigma1 t1 in let f1 = nf_evar sigma1 f1 in let a1 = Array.map (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 + 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 -> @@ -1018,7 +1019,7 @@ 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 @@ -1100,7 +1101,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = 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++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 @@ -1115,11 +1116,11 @@ 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 + | _ -> CoqConstr.fold aux acc t in aux [] (nf_evar sigma rp) in let sigma = List.fold_left (fun sigma e -> @@ -1202,7 +1203,7 @@ 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 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 *) @@ -1222,7 +1223,7 @@ 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 @@ -1407,7 +1408,7 @@ let () = let ssrinstancesof ist 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 concl = EConstr.Unsafe.to_constr concl in let sigma0, cpat = interp_cpattern ist gl arg None in diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 8e2a1a717..8ab666f7e 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -6,7 +6,7 @@ open Genarg open Tacexpr open Environ open Evd -open Term +open Constr (** ******** Small Scale Reflection pattern matching facilities ************* *) -- cgit v1.2.3