From 3a0b543af4ac99b29efdebe27b1d204d044a7bf0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 31 Mar 2018 17:43:18 +0200 Subject: Evar maps contain econstrs. We bootstrap the circular evar_map <-> econstr dependency by moving the internal EConstr.API module to Evd.MiniEConstr. Then we make the Evd functions use econstr. --- plugins/ssr/ssrcommon.ml | 16 +++++++++------- plugins/ssr/ssrelim.ml | 2 +- plugins/ssr/ssrequality.ml | 6 +++--- plugins/ssr/ssripats.ml | 2 +- plugins/ssr/ssrview.ml | 2 +- 5 files changed, 15 insertions(+), 13 deletions(-) (limited to 'plugins/ssr') diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index e07bc48a4..06c26edbe 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -509,11 +509,12 @@ let pf_abs_evars2 gl rigid (sigma, c0) = let nenv = env_size (pf_env gl) in let abs_evar n k = let evi = Evd.find sigma k in - let dc = CList.firstn n (evar_filtered_context evi) in + let concl = EConstr.Unsafe.to_constr evi.evar_concl in + let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in let abs_dc c = function | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c) | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in - let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in + let t = Context.Named.fold_inside abs_dc ~init:concl dc in nf_evar sigma t in let rec put evlist c = match Constr.kind c with | Evar (k, a) -> @@ -569,11 +570,12 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let nenv = env_size (pf_env gl) in let abs_evar n k = let evi = Evd.find sigma k in - let dc = CList.firstn n (evar_filtered_context evi) in + let concl = EConstr.Unsafe.to_constr evi.evar_concl in + let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in let abs_dc c = function | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c) | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in - let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in + let t = Context.Named.fold_inside abs_dc ~init:concl dc in nf_evar sigma0 (nf_evar sigma t) in let rec put evlist c = match Constr.kind c with | Evar (k, a) -> @@ -581,7 +583,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let n = max 0 (Array.length a - nenv) in let k_ty = Retyping.get_sort_family_of - (pf_env gl) sigma (EConstr.of_constr (Evd.evar_concl (Evd.find sigma k))) in + (pf_env gl) sigma (Evd.evar_concl (Evd.find sigma k)) in let is_prop = k_ty = InProp in let t = abs_evar n k in (k, (n, t, is_prop)) :: put evlist t | _ -> Constr.fold put evlist c in @@ -746,7 +748,7 @@ let pf_mkSsrConst name gl = let pf_fresh_global name gl = let sigma, env, it = project gl, pf_env gl, sig_it gl in let sigma,t = Evd.fresh_global env sigma name in - t, re_sig it sigma + EConstr.Unsafe.to_constr t, re_sig it sigma let mkProt t c gl = let prot, gl = pf_mkSsrConst "protect_term" gl in @@ -980,7 +982,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = if not (EConstr.Vars.closed0 sigma ty) then raise dependent_apply_error; let m = Evarutil.new_meta () in - loop (meta_declare m (EConstr.Unsafe.to_constr ty) sigma) bo ((EConstr.mkMeta m)::args) (n-1) + loop (meta_declare m ty sigma) bo ((EConstr.mkMeta m)::args) (n-1) | _ -> assert false in loop sigma t [] n in pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 717657a24..de8ffb976 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -356,7 +356,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let ev = List.fold_left Evar.Set.union Evar.Set.empty patterns_ev in let ty_ev = Evar.Set.fold (fun i e -> let ex = i in - let i_ty = EConstr.of_constr (Evd.evar_concl (Evd.find (project gl) ex)) in + let i_ty = Evd.evar_concl (Evd.find (project gl) ex) in Evar.Set.union e (evars_of_term i_ty)) ev Evar.Set.empty in let inter = Evar.Set.inter ev ty_ev in diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 2f0433b64..7748ba2b0 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -359,7 +359,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let evs = Evar.Set.elements (Evarutil.undefined_evars_of_term sigma t) in let open_evs = List.filter (fun k -> Sorts.InProp <> Retyping.get_sort_family_of - env sigma (EConstr.of_constr (Evd.evar_concl (Evd.find sigma k)))) + env sigma (Evd.evar_concl (Evd.find sigma k))) evs in if open_evs <> [] then Some name else None) (List.combine (Array.to_list args) names) @@ -478,10 +478,10 @@ let rwprocess_rule dir rule gl = | _ -> let ra = Array.append a [|r|] in function 1 -> let sigma, pi1 = Evd.fresh_global env sigma coq_prod.Coqlib.proj1 in - EConstr.mkApp (EConstr.of_constr pi1, ra), sigma + EConstr.mkApp (pi1, ra), sigma | _ -> let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in - EConstr.mkApp (EConstr.of_constr pi2, ra), sigma in + EConstr.mkApp (pi2, ra), sigma in if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_True ())) then let s, sigma = sr sigma 2 in loop (converse_dir d) sigma s a.(1) rs 0 diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index af78bf36a..6b7a96deb 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -623,7 +623,7 @@ let tacFIND_ABSTRACT_PROOF check_lock abstract_n = Goal.enter_one ~__LOC__ begin fun g -> let sigma, env = Goal.(sigma g, env g) in let l = Evd.fold_undefined (fun e ei l -> - match EConstr.kind sigma (EConstr.of_constr ei.Evd.evar_concl) with + match EConstr.kind sigma ei.Evd.evar_concl with | Term.App(hd, [|ty; n; lock|]) when (not check_lock || (occur_existential_or_casted_meta sigma ty && diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml index afe03533d..fc50b24a6 100644 --- a/plugins/ssr/ssrview.ml +++ b/plugins/ssr/ssrview.ml @@ -265,7 +265,7 @@ Goal.enter_one ~__LOC__ begin fun g -> List.fold_left (fun l k -> if Evd.is_defined sigma k then let bo = get_body Evd.(evar_body (find sigma k)) in - k :: l @ Evar.Set.elements (evars_of_econstr sigma bo) + k :: l @ Evar.Set.elements (evars_of_econstr sigma (EConstr.Unsafe.to_constr bo)) else l ) [] s in let und0 = (* Unassigned evars in the initial goal *) -- cgit v1.2.3