Allow partial-inlining in the inliner

This will allow fusing arithmetic simplification with constant inlining,
which is required for compilation to reified terms to work well, and
will hopefully eventually allow cleaning up the pipeline.

2 files changed, 16 insertions, 2 deletions

diff --git a/src/Compilers/Inline.v b/src/Compilers/Inline.v
index e4946adde..bd39b48a0 100644
--- a/src/Compilers/Inline.v
+++ b/src/Compilers/Inline.v
@@ -21,13 +21,20 @@ Section language.
     Inductive inline_directive : flat_type -> Type :=
     | default_inline {t} (e : @exprf var t) : inline_directive t
     | inline {t} (e : interp_flat_type (fun t => @exprf var (Tbase t)) t) : inline_directive t
-    | no_inline {t} (e : @exprf var t) : inline_directive t.
+    | no_inline {t} (e : @exprf var t) : inline_directive t
+    | partial_inline
+        {tx tC}
+        (ex : @exprf var tx)
+        (eC : interp_flat_type var tx -> interp_flat_type (fun t => @exprf var (Tbase t)) tC)
+      : inline_directive tC.
 
     Definition exprf_of_inline_directive {t} (v : inline_directive t) : @exprf var t
       := match v with
          | default_inline t e => e
          | inline t e => SmartPairf e
          | no_inline t e => e
+         | partial_inline _ _ ex eC
+           => LetIn ex (fun x => SmartPairf (eC x))
          end.
 
     Context (postprocess : forall {t}, @exprf var t -> inline_directive t).
@@ -45,6 +52,8 @@ Section language.
               | no_inline _ ex
                 => fun eC => LetIn ex (fun x => eC (SmartVarVarf x))
               | inline _ ex => fun eC => eC ex
+              | partial_inline _ _ ex eC'
+                => fun eC => LetIn ex (fun x => eC (eC' x))
               end (fun x => @inline_const_genf _ (eC x))
          | Var _ x => x
          | TT => TT
@@ -86,6 +95,7 @@ Global Arguments inline_directive {_} _ _ _, {_ _ _} _.
 Global Arguments no_inline {_ _ _ _} _.
 Global Arguments inline {_ _ _ _} _.
 Global Arguments default_inline {_ _ _ _} _.
+Global Arguments partial_inline {_ _ _ _ _} ex eC.
 Global Arguments inline_const_genf {_ _ _} postprocess {_} _.
 Global Arguments inline_const_gen {_ _ _} postprocess {_} _.
 Global Arguments InlineConstGen {_ _} postprocess {_} _ var.
diff --git a/src/Compilers/InlineWf.v b/src/Compilers/InlineWf.v
index 84bf07fb7..a9fc959d0 100644
--- a/src/Compilers/InlineWf.v
+++ b/src/Compilers/InlineWf.v
@@ -33,10 +33,12 @@ Section language.
             | default_inline _ _, default_inline _ _
             | no_inline _ _, no_inline _ _
             | inline _ _, inline _ _
+            | partial_inline _ _ _ _, partial_inline _ _ _ _
               => True
             | default_inline _ _, _
             | no_inline _ _, _
             | inline _ _, _
+            | partial_inline _ _ _ _, _
               => False
             end) x y).
 
@@ -118,7 +120,7 @@ Section language.
              | _ => progress inversion_sigma
              | _ => progress inversion_prod
              | _ => progress destruct_head' and
-             | _ => inversion_wf_step; progress subst
+             | _ => inversion_wf_step; destruct_head' sig; progress subst
              | _ => progress specialize_by_assumption
              | _ => progress break_match
              | _ => progress invert_inline_directive
@@ -150,6 +152,8 @@ Section language.
         intros; destruct_head or; t_fin. }
       { match goal with H : _ |- _ => apply H end.
         intros; destruct_head or; t_fin. }
+      { match goal with H : _ |- _ => apply H end.
+        intros; destruct_head or; t_fin. }
     Qed.
 
     Lemma wff_postprocess_for_const is_const G t