Factor lift_existT into expr_to_pattern_and_replacement_unfolded{,_sp…

…lit} in reify_to_pattern_and_replacement_in_context <details><summary>Timing Diff</summary> <p> ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- 4m10.43s | 1406768 ko | Total Time / Peak Mem | 4m10.13s | 1419076 ko || +0m00.30s || -12308 ko | +0.11% | -0.86% ---------------------------------------------------------------------------------------------------------------------------------------------------------------------- 0m55.77s | 1406768 ko | Rewriter/Rewriter/Examples/PerfTesting/SieveOfEratosthenes.vo | 0m55.70s | 1419076 ko || +0m00.07s || -12308 ko | +0.12% | -0.86% 0m55.15s | 1119396 ko | Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.vo | 0m55.30s | 1109780 ko || -0m00.14s || 9616 ko | -0.27% | +0.86% 0m53.75s | 1072204 ko | Rewriter/Rewriter/Examples.vo | 0m53.46s | 1070164 ko || +0m00.28s || 2040 ko | +0.54% | +0.19% 0m30.00s | 927484 ko | Rewriter/Rewriter/Examples/PrefixSums.vo | 0m30.08s | 923084 ko || -0m00.07s || 4400 ko | -0.26% | +0.47% 0m23.91s | 882200 ko | Rewriter/Rewriter/Examples/PerfTesting/Plus0Tree.vo | 0m23.96s | 885260 ko || -0m00.05s || -3060 ko | -0.20% | -0.34% 0m16.06s | 734968 ko | Rewriter/Rewriter/Examples/PerfTesting/UnderLetsPlus0.vo | 0m15.91s | 735200 ko || +0m00.14s || -232 ko | +0.94% | -0.03% 0m12.07s | 636716 ko | Rewriter/Demo.vo | 0m12.08s | 640800 ko || -0m00.00s || -4084 ko | -0.08% | -0.63% 0m00.85s | 475472 ko | Rewriter/Rewriter/Reify.vo | 0m00.82s | 473124 ko || +0m00.03s || 2348 ko | +3.65% | +0.49% 0m00.82s | 488764 ko | Rewriter/Rewriter/AllTactics.vo | 0m00.75s | 488668 ko || +0m00.06s || 96 ko | +9.33% | +0.01% 0m00.57s | 482324 ko | Rewriter/Rewriter/Examples/PerfTesting/Settings.vo | 0m00.48s | 482352 ko || +0m00.08s || -28 ko | +18.74% | -0.00% 0m00.56s | 480404 ko | Rewriter/Util/plugins/RewriterBuild.vo | 0m00.56s | 480516 ko || +0m00.00s || -112 ko | +0.00% | -0.02% 0m00.47s | 480232 ko | Rewriter/Util/plugins/RewriterBuildRegistry.vo | 0m00.50s | 480216 ko || -0m00.03s || 16 ko | -6.00% | +0.00% 0m00.46s | 478952 ko | Rewriter/Util/plugins/RewriterBuildRegistryImports.vo | 0m00.54s | 479076 ko || -0m00.08s || -124 ko | -14.81% | -0.02% ``` </p> </details>
mit-plv · Oct 2, 2022 · 499ea11 · 499ea11
1 parent 86dc030
commit 499ea11
Showing 1 changed file with 8 additions and 9 deletions.
diff --git a/src/Rewriter/Rewriter/Reify.v b/src/Rewriter/Rewriter/Reify.v
@@ -202,9 +202,10 @@ Module Compilers.
                          else None))).
 
         (** N.B. We must annotate the type of [invalid] to relax universe constraints *)
-        Definition expr_to_pattern_and_replacement_unfolded gets_inlined should_do_again evm {t} lhs rhs side_conditions (invalid : forall A B : Type, A -> B)
+        Definition expr_to_pattern_and_replacement_unfolded_split gets_inlined should_do_again evm {t} lhs rhs side_conditions
           := Eval cbv beta iota delta [expr_to_pattern_and_replacement lookup_expr_gets_inlined pattern_of_expr lam_unification_resultT' Pos.succ pair'_unification_resultT' PositiveMap.empty PositiveMap.fold Pos.max expr_pos_to_expr_value (* expr_value_to_rewrite_rule_replacement*) fold_left List.rev List.app value PositiveMap.add PositiveMap.xfoldi Pos.compare Pos.compare_cont FMapPositive.append projT1 projT2 PositiveMap.find Base_value (*UnderLets.map reify_expr_beta_iota reflect_expr_beta_iota*) lam_type_of_list fold_right list_rect pattern.type.relax pattern.type.subst_default pattern.type.subst_default_relax pattern.type.unsubst_default_relax option_map unification_resultT' with_unification_resultT' with_unif_rewrite_ruleTP_gen']
-            in @expr_to_pattern_and_replacement gets_inlined should_do_again evm invalid t lhs rhs side_conditions.
+            in let f := fun (invalid : forall A B : Type, A -> B) => @expr_to_pattern_and_replacement gets_inlined should_do_again evm invalid t lhs rhs side_conditions in
+               existT _ (fun invalid => projT1 (f invalid)) (fun invalid => projT2 (f invalid)).
 
         Definition partial_lam_unif_rewrite_ruleTP_gen_unfolded should_do_again {t} p
           := Eval cbv beta iota delta [partial_lam_unif_rewrite_ruleTP_gen pattern.collect_vars pattern.type.lam_forall_vars partial_lam_unification_resultT pattern.type.collect_vars pattern.base.collect_vars PositiveSet.union PositiveSet.add PositiveSet.empty pattern.type.lam_forall_vars_gen List.rev PositiveSet.elements PositiveSet.xelements PositiveSet.rev PositiveSet.rev_append List.app orb fold_right PositiveMap.add PositiveMap.empty]
@@ -827,8 +828,6 @@ Module Compilers.
           (fun () => Control.refine
                        (fun () => adjust_side_conditions_for_gets_inlined' value_ctx side_conditions (mkVar lookup_gets_inlined))).
 
-      Definition lift_existT {X A B} (v : forall x : X, @sigT (A x) (B x))
-        := Eval cbv [projT1 projT2] in existT _ (fun x => projT1 (v x)) (fun x => projT2 (v x)).
       Ltac2 rec reify_to_pattern_and_replacement_in_context (base : constr) (reify_base : constr -> constr) (base_interp : constr) (base_interp_beq : constr) (try_make_transport_base_cps : constr) (ident : constr) (reify_ident_opt : binder list -> constr -> constr option) (pident : constr) (pident_arg_types : constr) (pident_type_of_list_arg_types_beq : constr) (pident_of_typed_ident : constr) (pident_arg_types_of_typed_ident : constr) (reflect_ident_iota : constr) (avoid : Fresh.Free.t) (type_ctx : constr) (var : constr) (gets_inlined : constr) (should_do_again : constr) (cur_i : constr) (term : constr) (value_ctx : (ident * constr (* ty *) * constr (* var *)) list) : constr :=
         Reify.debug_wrap
           "reify_to_pattern_and_replacement_in_context" Message.of_constr term
@@ -859,7 +858,7 @@ Module Compilers.
                    | (@eq ?t ?a ?b, ?side_conditions)
                      => let base_interp_head := head_reference base_interp in
                         let var_pos := '(fun _ : type $base_type => positive) in
-                        let cexpr_to_pattern_and_replacement_unfolded := debug_Constr_check (fun () => mkApp '@expr_to_pattern_and_replacement_unfolded [base; try_make_transport_base_cps; ident; var; pident; pident_arg_types; pident_type_of_list_arg_types_beq; pident_of_typed_ident; pident_arg_types_of_typed_ident; mkApp reflect_ident_iota [var]; gets_inlined; should_do_again; type_ctx]) in
+                        let cexpr_to_pattern_and_replacement_unfolded_split := debug_Constr_check (fun () => mkApp '@expr_to_pattern_and_replacement_unfolded_split [base; try_make_transport_base_cps; ident; var; pident; pident_arg_types; pident_type_of_list_arg_types_beq; pident_of_typed_ident; pident_arg_types_of_typed_ident; mkApp reflect_ident_iota [var]; gets_inlined; should_do_again; type_ctx]) in
                         let cpartial_lam_unif_rewrite_ruleTP_gen := debug_Constr_check (fun () => mkApp '@partial_lam_unif_rewrite_ruleTP_gen_unfolded [base; ident; var; pident; pident_arg_types; should_do_again]) in
                         let value := debug_Constr_check (fun () => mkApp '@value [base_type; ident; var]) in
                         let cinvalidT := '(forall A B : Type, A -> B) in
@@ -880,17 +879,17 @@ Module Compilers.
                         let rA := expr.reify_in_context base_type ident reify_base_type reify_ident_opt var_pos a [] [] value_ctx [] None in
                         let rB := expr.reify_in_context base_type ident reify_base_type reify_ident_opt var_pos b [] [] value_ctx [] None in
                         let side_conditions := adjust_side_conditions_for_gets_inlined avoid value_ctx side_conditions in
-                        (* N.B. We need both check and η-expansion here to ... relax universe constraints? *)
+                        (* N.B. We need check here to ... relax universe constraints? *)
                         let res := check "res"
-                                         (fun () => mkApp cexpr_to_pattern_and_replacement_unfolded [rT; rA; rB; side_conditions]) in
+                                         (fun () => mkApp cexpr_to_pattern_and_replacement_unfolded_split [rT; rA; rB; side_conditions]) in
                         let res := let pident_arg_types := head_reference pident_arg_types in
                                    let pident_of_typed_ident := head_reference pident_of_typed_ident in
                                    let pident_type_of_list_arg_types_beq := head_reference pident_type_of_list_arg_types_beq in
                                    let pident_arg_types_of_typed_ident := head_reference pident_arg_types_of_typed_ident in
-                                   (eval cbv [expr_to_pattern_and_replacement_unfolded $pident_arg_types $pident_of_typed_ident $pident_type_of_list_arg_types_beq $pident_arg_types_of_typed_ident (*reflect_ident_iota*)] in res) in
+                                   (eval cbv [expr_to_pattern_and_replacement_unfolded_split $pident_arg_types $pident_of_typed_ident $pident_type_of_list_arg_types_beq $pident_arg_types_of_typed_ident (*reflect_ident_iota*)] in res) in
                         let res := (eval cbn [fst snd andb pattern.base.relax pattern.base.subst_default pattern.base.subst_default_relax] in res) in
                         let res := change_pattern_base_subst_default_relax res in
-                        let (p, res) := lazy_match! (eval cbv [lift_existT] in constr:(@lift_existT _ _ _ $res)) with
+                        let (p, res) := lazy_match! res with
                                         | existT _ ?p ?res => (p, res)
                                         end in
                         let p := strip_invalid_or_fail p in