Remove thunking from abstract interpretation

It was a premature optimization

After     | File Name                                            | Before    || Change    | % Change
----------------------------------------------------------------------------------------------------
12m57.07s | Total                                                | 12m59.91s || -0m02.84s | -0.36%
----------------------------------------------------------------------------------------------------
5m49.37s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples   | 5m49.86s  || -0m00.49s | -0.14%
4m31.64s  | Experiments/NewPipeline/Toplevel1                    | 4m32.60s  || -0m00.96s | -0.35%
1m33.27s  | Experiments/NewPipeline/Toplevel2                    | 1m33.94s  || -0m00.66s | -0.71%
0m44.30s  | Experiments/NewPipeline/AbstractInterpretationProofs | 0m44.73s  || -0m00.42s | -0.96%
0m12.60s  | Experiments/NewPipeline/CStringification             | 0m12.60s  || +0m00.00s | +0.00%
0m01.38s  | Experiments/NewPipeline/CLI                          | 0m01.37s  || +0m00.00s | +0.72%
0m01.24s  | Experiments/NewPipeline/StandaloneHaskellMain        | 0m01.39s  || -0m00.14s | -10.79%
0m01.12s  | Experiments/NewPipeline/StandaloneOCamlMain          | 0m01.22s  || -0m00.09s | -8.19%
0m01.11s  | Experiments/NewPipeline/AbstractInterpretation       | 0m01.14s  || -0m00.02s | -2.63%
0m01.04s  | Experiments/NewPipeline/CompilersTestCases           | 0m01.07s  || -0m00.03s | -2.80%

2 files changed, 16 insertions, 86 deletions

diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v
index b6c6c4004..8f55400a3 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretation.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretation.v
@@ -684,22 +684,6 @@ Module Compilers.
 
       Context (interp_ident : forall t, ident t -> value_with_lets t).
 
-      Definition lazy_abstract_domain (t : type)
-        := type.interp (fun t => unit -> abstract_domain' t) t.
-
-      Fixpoint force_abstract_domain {t} : lazy_abstract_domain t -> abstract_domain t
-        := match t with
-           | type.base t => fun st => st tt
-           | type.arrow s d
-             => fun f x => @force_abstract_domain d (f (@thunk_abstract_domain s x))
-           end
-      with thunk_abstract_domain {t} : abstract_domain t -> lazy_abstract_domain t
-           := match t with
-              | type.base t => fun st (_ : unit) => st
-              | type.arrow s d
-                => fun f x => @thunk_abstract_domain d (f (@force_abstract_domain s x))
-              end.
-
       Fixpoint bottom {t} : abstract_domain t
         := match t with
            | type.base t => bottom' t
@@ -780,27 +764,14 @@ Module Compilers.
         := UnderLets.to_expr (reify false (reflect e bottom) st).
 
       Section extract.
-        Context (ident_extract : forall t, ident t -> lazy_abstract_domain t).
+        Context (ident_extract : forall t, ident t -> abstract_domain t).
 
-        Fixpoint extract' {t} (e : @expr lazy_abstract_domain t)
-          : lazy_abstract_domain t
-          := match e in expr.expr t return lazy_abstract_domain t with
-             | expr.Ident t idc => ident_extract t idc
-             | expr.Var t v => v
-             | expr.Abs s d f
-               => fun v => @extract' d (f v)
-             | expr.App s d f x
-               => let f' := @extract' _ f in
-                  let x' := @extract' _ x in
-                  f' x'
-             | expr.LetIn A B x f
-               => let x' := @extract' A x in
-                  @extract' B (f x')
-             end.
+        Definition extract' {t} (e : @expr abstract_domain t) : abstract_domain t
+          := expr.interp (@ident_extract) e.
 
-        Definition extract_gen {t} (e : @expr lazy_abstract_domain t) (bound : type.for_each_lhs_of_arrow abstract_domain t)
+        Definition extract_gen {t} (e : @expr abstract_domain t) (bound : type.for_each_lhs_of_arrow abstract_domain t)
           : abstract_domain' (type.final_codomain t)
-          := type.app_curried (extract' e) (type.map_for_each_lhs_of_arrow (@thunk_abstract_domain) bound) tt.
+          := type.app_curried (extract' e) bound.
       End extract.
     End with_var.
 
@@ -943,21 +914,19 @@ Module Compilers.
           := @eta_expand_with_bound' base.type ident var abstract_domain' annotate bottom' t e st.
 
         Section extract.
-          Local Notation lazy_abstract_domain := (@lazy_abstract_domain base.type abstract_domain').
-          Local Notation thunk_abstract_domain := (@thunk_abstract_domain base.type abstract_domain').
           Local Notation bottom := (@bottom base.type abstract_domain' bottom').
-          Definition ident_extract {t} (idc : ident t) : lazy_abstract_domain t
-            := match idc in ident.ident t return lazy_abstract_domain t with
+          Definition ident_extract {t} (idc : ident t) : abstract_domain t
+            := match idc in ident.ident t return abstract_domain t with
                | ident.Literal _ _ as idc
                | ident.nil _ as idc
                | ident.cons _ as idc
                | ident.pair _ _ as idc
-                 => thunk_abstract_domain (abstract_interp_ident _ idc)
+                 => abstract_interp_ident _ idc
                | ident.Z_cast _ as idc
                | ident.Z_cast2 _ as idc
                  => (* fast-path for cast: don't bother with the abstract state of the argument *)
-                 fun _ 'tt => abstract_interp_ident _ idc (bottom' _)
-               | _ => thunk_abstract_domain bottom
+                 fun _ => abstract_interp_ident _ idc (bottom' _)
+               | _ => bottom
                end.
 
           Definition extract {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t)
diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
index d9c74e73e..f806aea25 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
@@ -269,38 +269,6 @@ Module Compilers.
           eapply UnderLets.wf_to_expr, wf_reify; [ eapply wf_reflect | ]; eauto; apply bottom_Proper.
         Qed.
 
-        Local Notation lazy_abstract_domain := (@lazy_abstract_domain base_type abstract_domain').
-        Local Notation force_abstract_domain := (@force_abstract_domain base_type abstract_domain').
-        Local Notation thunk_abstract_domain := (@thunk_abstract_domain base_type abstract_domain').
-
-        Definition lazy_abstract_domain'_R {t} : relation (lazy_abstract_domain (type.base t))
-          := fun v1 v2 => abstract_domain'_R t (force_abstract_domain v1) (force_abstract_domain v2).
-        Definition lazy_abstract_domain_R {t} : relation (lazy_abstract_domain t)
-          := fun v1 v2 => abstract_domain_R (force_abstract_domain v1) (force_abstract_domain v2).
-
-        Local Ltac red_thunk_force' s d :=
-          change (@force_abstract_domain (s -> d)) with (fun f x => @force_abstract_domain d (f (@thunk_abstract_domain s x))) in *;
-          change (@thunk_abstract_domain (s -> d)) with (fun f x => @thunk_abstract_domain d (f (@force_abstract_domain s x))) in *.
-        Local Ltac red_thunk_force :=
-          repeat match goal with
-                 | [ |- context[@force_abstract_domain (type.arrow ?s ?d)] ] => progress red_thunk_force' s d
-                 | [ |- context[@thunk_abstract_domain (type.arrow ?s ?d)] ] => progress red_thunk_force' s d
-                 | [ H : context[@force_abstract_domain (type.arrow ?s ?d)] |- _ ] => progress red_thunk_force' s d
-                 | [ H : context[@thunk_abstract_domain (type.arrow ?s ?d)] |- _ ] => progress red_thunk_force' s d
-                 end;
-          cbv beta in *.
-
-        Lemma force_thunk_abstract_domain {t} : (fun v => @force_abstract_domain t (thunk_abstract_domain v)) = (fun v => v).
-        Proof.
-          induction t as [t|s IHs d IHd]; [ reflexivity | ].
-          change
-            ((fun (v : abstract_domain (s -> d)) (x : abstract_domain s)
-              => id (fun v => force_abstract_domain (thunk_abstract_domain v)) (v (id (fun v => force_abstract_domain (thunk_abstract_domain v)) x)))
-             = (fun v => v)).
-          rewrite IHs, IHd; cbv [id]; reflexivity.
-        Qed.
-        Lemma force_thunk_abstract_domain_ext {t} v : @force_abstract_domain t (thunk_abstract_domain v) = v.
-        Proof. exact (f_equal (fun f => f v) force_thunk_abstract_domain). Qed.
         (*
         Lemma related_force {t} x y
           : @lazy_abstract_domain_R t x y <-> @abstract_domain_R t (force_abstract_domain x) (force_abstract_domain y).
@@ -792,26 +760,19 @@ Module Compilers.
 
           Section extract.
             Local Notation ident_extract := (@ident.ident_extract abstract_domain' bottom' abstract_interp_ident).
-            Local Notation lazy_abstract_domain_R := (@lazy_abstract_domain_R base.type abstract_domain' abstract_domain'_R).
             Global Instance ident_extract_Proper {t}
-              : Proper (eq ==> lazy_abstract_domain_R) (@ident_extract t).
+              : Proper (eq ==> abstract_domain_R) (@ident_extract t).
             Proof.
               intros idc idc' ?; subst idc'.
-              destruct idc; cbn [ident.ident_extract]; cbv [lazy_abstract_domain_R];
-                repeat first [ match goal with
-                               | [ |- context G[force_abstract_domain _ (thunk_abstract_domain _ ?x)] ]
-                                 => let G' := context G [x] in
-                                   change G'
-                               | [ |- context G[force_abstract_domain _ (fun _ 'tt => ?x)] ]
-                                 => cbv [force_abstract_domain abstract_domain_R]
-                               end
-                             | refine (abstract_interp_ident_Proper _ _ _ eq_refl)
+              destruct idc; cbn [ident.ident_extract];
+                repeat first [ refine (abstract_interp_ident_Proper _ _ _ eq_refl)
                              | eapply bottom_Proper
                              | eapply bottom'_Proper
-                             | progress cbn [type.related]
+                             | progress cbn [type.related abstract_domain'_R]
                              | progress cbv [respectful]
                              | progress intros
-                             | refine (abstract_interp_ident_Proper (type.arrow (type.base _) (type.base _)) _ _ eq_refl _ _ _) ].
+                             | refine (abstract_interp_ident_Proper (type.arrow (type.base _) (type.base _)) _ _ eq_refl _ _ _)
+                             | progress cbv [type.related abstract_domain_R] ].
             Qed.
 
           (*