From d7a6fd5fd04ebc314bfd3129afb909cfddc4f6ee Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Sun, 2 Jun 2024 21:44:22 +0200 Subject: [PATCH 1/5] Further reduction of useless typing in solution. --- src/simplify.ml | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/src/simplify.ml b/src/simplify.ml index 90492824..43f22a9e 100644 --- a/src/simplify.ml +++ b/src/simplify.ml @@ -352,6 +352,11 @@ let build_term ~where (env : Environ.env) (evd : Evd.evar_map ref) (gl : goal) ( in ans, c +let checked_applist env evd hd args = + evd_comb0 (fun sigma -> Typing.checked_applist env sigma hd args) evd +let checked_appvect env evd hd args = + evd_comb0 (fun sigma -> Typing.checked_appvect env sigma hd args) evd + let build_app_infer_concl (env : Environ.env) (evd : Evd.evar_map ref) ((ctx, _, u) : goal) (f : Names.GlobRef.t) ?(inst:EInstance.t option) (args : EConstr.constr option list) = @@ -385,7 +390,7 @@ let build_app_infer_concl (env : Environ.env) (evd : Evd.evar_map ref) ((ctx, _, in let env = push_rel_context ctx env in let prefix, suffix = CList.map_until (fun o -> o) args in - let hd = evd_comb0 (fun sigma -> Typing.checked_applist env sigma tf prefix) evd in + let hd = checked_applist env evd tf prefix in let rec aux ty args = match kind !evd ty, args with | Constr.Prod (_, t, c), hd :: tl -> aux (Vars.subst1 hd c) tl @@ -399,7 +404,7 @@ let build_app_infer_concl (env : Environ.env) (evd : Evd.evar_map ref) ((ctx, _, (* let u = Retyping.get_sort_of env !evd ty' in *) let cont = fun c -> let suffix = CList.map (Option.default c) suffix in - evd_comb0 (fun sigma -> Typing.checked_applist env sigma hd suffix) evd + checked_applist env evd hd suffix in cont, ty', u (** Same as above but assumes that the arguments are well-typed in [ctx]. This @@ -794,7 +799,7 @@ SimpFun.make ~name:"solution" begin fun (env : Environ.env) (evd : Evd.evar_map Vars.substnl [Vars.lift (-rel') term'] (pred rel') body else let teq_refl = EConstr.mkApp (Builder.eq_refl equ, [| tA'; term' |]) in - Vars.substnl [Vars.lift (-rel') teq_refl; Vars.lift (-rel') term'] (pred rel') body + Vars.substnl [Vars.lift (-rel') teq_refl; Vars.lift (-rel') term'] (pred rel') body in let lsubst = Context_map.single_subst env !evd rel' (Context_map.pat_of_constr env !evd term') ctx' in let subst = Context_map.compose_subst env ~sigma:!evd lsubst subst in @@ -804,22 +809,24 @@ SimpFun.make ~name:"solution" begin fun (env : Environ.env) (evd : Evd.evar_map (* [c] is a term in the context [before']. *) let c = Vars.lift rel' c in (* [c] is a term in the context [ctx']. *) + let env = push_rel_context ctx' env in let c = if nondep then - EConstr.mkApp (tsolution, [| tA'; tB'; term'; c; trel' |]) + checked_appvect env evd tsolution [| tA'; tB'; term'; c; trel' |] else - EConstr.mkApp (tsolution, [| tA'; term'; tB'; c; trel' |]) + checked_appvect env evd tsolution [| tA'; term'; tB'; c; trel' |] in (* We make some room for the application of the equality... *) + let env = push_rel (LocalAssum (name, ty1')) env in let c = Vars.lift 1 c in - let c = EConstr.mkApp (c, [| EConstr.mkRel 1 |]) in + let c = checked_appvect env evd c [| EConstr.mkRel 1 |] in (* [targs'] are arguments in the context [eq_decl :: ctx']. *) - let c = EConstr.mkApp (c, targs') in + let c = checked_appvect env evd c targs' in (* [ty1'] is the type of the equality in [ctx']. *) let c = EConstr.mkLambda (name, ty1', c) in (* And now we recover a term in the context [ctx]. *) - Context_map.mapping_constr !evd rev_subst c - in build_term ~where:"[solution]" env evd (ctx, ty, glu) (ctx'', ty'', glu') f, true, subst + Context_map.mapping_constr !evd rev_subst c + in build_term_core env evd (ctx'', ty'', glu') f, true, subst end let whd_all env sigma t = From 9127f6177863ef677b7a2f3eacea92bae0347c42 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Fri, 7 Jun 2024 16:18:21 +0200 Subject: [PATCH 2/5] Remove useless typechecking from hnf. --- src/simplify.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/simplify.ml b/src/simplify.ml index 43f22a9e..accd3b59 100644 --- a/src/simplify.ml +++ b/src/simplify.ml @@ -589,7 +589,8 @@ let hnf_goal ~(reduce_equality:bool) = let equ, tA, t1, t2 = check_equality env !evd ctx ty1 in let t1 = reduce t1 in let t2 = reduce t2 in - let ty1 = EConstr.mkApp (Builder.equ equ, [| tA; t1; t2 |]) in + let env = push_rel_context ctx env in + let ty1 = checked_appvect env evd (Builder.equ equ) [| tA; t1; t2 |] in EConstr.mkProd (name, ty1, ty2) with CannotSimplify _ -> ty else ty @@ -600,7 +601,7 @@ let hnf_goal ~(reduce_equality:bool) = let hnf ~reduce_equality : simplification_fun = SimpFun.make ~name:"hnf" begin fun (env : Environ.env) (evd : Evd.evar_map ref) ((ctx, ty, u as gl) : goal) -> let gl' = hnf_goal ~reduce_equality env evd gl in - build_term ~where:"[hnf]" env evd gl gl' (fun c -> c), true, Context_map.id_subst ctx + build_term_core env evd gl' (fun c -> c), true, Context_map.id_subst ctx end let with_retry (f : simplification_fun) : simplification_fun = From e8a31032e12a52c033ac73b6cfeb1687cf09ac98 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Fri, 7 Jun 2024 16:20:14 +0200 Subject: [PATCH 3/5] Remove more useless typing from pre_solution and deletion. --- src/simplify.ml | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/src/simplify.ml b/src/simplify.ml index accd3b59..31221676 100644 --- a/src/simplify.ml +++ b/src/simplify.ml @@ -489,12 +489,6 @@ SimpFun.make ~name:"guard_block" begin fun (env : Environ.env) (evd : Evd.evar_m else SimpFun.apply f env evd gl end -(* let remove_block : simplification_fun = -SimpFun.make ~name:"remove_block" begin fun (env : Environ.env) (evd : Evd.evar_map ref) ((ctx, ty, glu) : goal) -> - let _na, b, _ty, b' = check_letin !evd ty in - build_term env evd (ctx, ty, glu) (ctx, Vars.subst1 b b', glu) (fun c -> c), true, Context_map.id_subst ctx -end *) - let identity : simplification_fun = SimpFun.make ~name:"identity" begin fun (env : Environ.env) (evd : Evd.evar_map ref) ((ctx, ty, u as gl) : goal) -> build_term_core env evd gl (fun c -> c), true, Context_map.id_subst ctx @@ -696,7 +690,7 @@ SimpFun.make ~name:"deletion" begin fun (env : Environ.env) (evd : Evd.evar_map let subst = Context_map.id_subst ctx in if Vars.noccurn !evd 1 ty2 then (* The goal does not depend on the equality, we can just eliminate it. *) - build_term ~where:"[deletion]" env evd (ctx, ty, glu) (ctx, Termops.pop ty2, glu) + build_term_core env evd (ctx, Termops.pop ty2, glu) (fun c -> EConstr.mkLambda (name, ty1, Vars.lift 1 c)), true, subst else @@ -870,11 +864,12 @@ SimpFun.make ~name:"pre_solution" begin fun (env : Environ.env) (evd : Evd.evar_ let f c = c in let eqf, _ = Equations_common.decompose_appvect !evd ty1 in let ty1 = - if var_left then mkApp (eqf, [| tA; trel; term |]) - else mkApp (eqf, [| tA; term; trel |]) + let env = push_rel_context ctx env in + if var_left then checked_appvect env evd eqf [| tA; trel; term |] + else checked_appvect env evd eqf [| tA; term; trel |] in let ty' = mkProd (name, ty1, ty2) in - build_term ~where:"[pre_solution]" env evd (ctx, ty, glu) (ctx, ty', glu) f, true, Context_map.id_subst ctx + build_term_core env evd (ctx, ty', glu) f, true, Context_map.id_subst ctx end let pre_solution ~(dir:direction) = with_retry (pre_solution ~dir) From c24773a24a541cfdc944a8943d76d896f6fbdce0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Fri, 7 Jun 2024 16:31:07 +0200 Subject: [PATCH 4/5] Remove the last call to build_term in Simplify. --- src/simplify.ml | 19 +------------------ 1 file changed, 1 insertion(+), 18 deletions(-) diff --git a/src/simplify.ml b/src/simplify.ml index 31221676..3d5761ff 100644 --- a/src/simplify.ml +++ b/src/simplify.ml @@ -335,23 +335,6 @@ let build_term_core (env : Environ.env) (evd : Evd.evar_map ref) let ev = EConstr.destEvar !evd tev in Some (ngl, ev), c -(* Build a term with an evar out of [constr -> constr] function. *) -let build_term ~where (env : Environ.env) (evd : Evd.evar_map ref) (gl : goal) (ngl : goal) f : open_term = - let ans, c = build_term_core env evd ngl f in - let (ctx, _, _) = gl in - let env = push_rel_context ctx env in - let _ = - try Equations_common.evd_comb1 (Typing.type_of env) evd c - with Type_errors.TypeError (env, tyerr) -> - anomaly Pp.(str where ++ spc () ++ str "Equations build an ill-typed term: " ++ Printer.pr_econstr_env env !evd c ++ fnl () ++ - Himsg.explain_pretype_error env !evd - (Pretype_errors.TypingError (Pretype_errors.of_type_error tyerr))) - | Pretype_errors.PretypeError (env, evd, tyerr) -> - anomaly Pp.(str where ++ spc () ++ str "Equations build an ill-typed term: " ++ Printer.pr_econstr_env env evd c ++ fnl () ++ - Himsg.explain_pretype_error env evd tyerr) - in - ans, c - let checked_applist env evd hd args = evd_comb0 (fun sigma -> Typing.checked_applist env sigma hd args) evd let checked_appvect env evd hd args = @@ -1088,7 +1071,7 @@ SimpFun.make ~name:"elim_true" begin fun (env : Environ.env) (evd : Evd.evar_map (* Check if the goal is dependent or not. *) if Vars.noccurn !evd 1 ty2 then (* Not dependent, we can just eliminate True. *) - build_term ~where:"[elim_true]" env evd (ctx, ty, glu) (ctx, Termops.pop ty2, glu) + build_term_core env evd (ctx, Termops.pop ty2, glu) (fun c -> EConstr.mkLambda (name, ty1, Vars.lift 1 c)), true, subst else (* Apply the dependent induction principle for True. *) From 7750eb70dea3756483e6324b7291dd350872b3fe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Fri, 7 Jun 2024 16:34:07 +0200 Subject: [PATCH 5/5] Last undue call to typing in elim_false. --- src/simplify.ml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/simplify.ml b/src/simplify.ml index 3d5761ff..5e61fe73 100644 --- a/src/simplify.ml +++ b/src/simplify.ml @@ -1113,12 +1113,8 @@ SimpFun.make ~name:"elim_false" begin fun (env : Environ.env) (evd : Evd.evar_ma else let sigma, equ, glu = Equations_common.instance_of env !evd glu in evd := sigma; equ, glu in - let c = EConstr.mkApp (EConstr.mkRef (tzero_ind, inst), [| tB |]) in - (* We need to type the term in order to solve eventual universes - * constraints. *) - let _ = let env = push_rel_context ctx env in - Equations_common.evd_comb1 (Typing.type_of env) evd c in - (None, c), true, subst + let c = checked_appvect (push_rel_context ctx env) evd (EConstr.mkRef (tzero_ind, inst)) [| tB |] in + (None, c), true, subst end let elim_false = with_retry elim_false