Generalize InlineConst

Should now support constant subexpression evaluation (removing things
like (_ + 0)).

1 files changed, 21 insertions, 12 deletions

diff --git a/src/Reflection/Inline.v b/src/Reflection/Inline.v
index a565835b0..e10b7c1ea 100644
--- a/src/Reflection/Inline.v
+++ b/src/Reflection/Inline.v
@@ -14,37 +14,46 @@ Section language.
   Local Coercion Tbase : base_type_code >-> Syntax.flat_type.
   Let interp_type := interp_type interp_base_type.
   Let interp_flat_type := interp_flat_type_gen interp_base_type.
+  Local Notation exprf := (@exprf base_type_code interp_base_type op).
+  Local Notation expr := (@expr base_type_code interp_base_type op).
   Local Notation Expr := (@Expr base_type_code interp_base_type op).
 
   Section with_var.
     Context {var : base_type_code -> Type}.
-    Local Notation exprf := (@exprf base_type_code interp_base_type op).
-    Local Notation expr := (@expr base_type_code interp_base_type op).
+    Context (postprocess : forall {t}, @exprf var t -> @exprf var t).
 
-    Fixpoint inline_constf {t} (e : @exprf (@exprf var) t) : @exprf var t
+    Fixpoint inline_const_genf {t} (e : @exprf (@exprf var) t) : @exprf var t
       := match e in Syntax.exprf _ _ _ t return @exprf var t with
          | Let _ ex tC eC
-           => match @inline_constf _ ex in Syntax.exprf _ _ _ t' return (interp_flat_type_gen _ t' -> @exprf var tC) -> @exprf var tC with
+           => match postprocess _ (@inline_const_genf _ ex) in Syntax.exprf _ _ _ t' return (interp_flat_type_gen _ t' -> @exprf var tC) -> @exprf var tC with
               | Const _ x => fun eC => eC (SmartConst (op:=op) (var:=var) x)
+              | Var _ x => fun eC => eC (Var x)
               | ex => fun eC => Let ex (fun x => eC (SmartVarVar x))
-              end (fun x => @inline_constf _ (eC x))
+              end (fun x => @inline_const_genf _ (eC x))
          | Var _ x => x
          | Const _ x => Const x
-         | Pair _ ex _ ey => Pair (@inline_constf _ ex) (@inline_constf _ ey)
-         | Op _ _ op args => Op op (@inline_constf _ args)
+         | Pair _ ex _ ey => Pair (@inline_const_genf _ ex) (@inline_const_genf _ ey)
+         | Op _ _ op args => Op op (@inline_const_genf _ args)
          end.
 
-    Fixpoint inline_const {t} (e : @expr (@exprf var) t) : @expr var t
+    Fixpoint inline_const_gen {t} (e : @expr (@exprf var) t) : @expr var t
       := match e in Syntax.expr _ _ _ t return @expr var t with
-         | Return _ x => Return (inline_constf x)
-         | Abs _ _ f => Abs (fun x => @inline_const _ (f (Var x)))
+         | Return _ x => Return (inline_const_genf x)
+         | Abs _ _ f => Abs (fun x => @inline_const_gen _ (f (Var x)))
          end.
   End with_var.
+  Definition inline_constf {var t} := @inline_const_genf var (fun _ x => x) t.
+  Definition inline_const {var t} := @inline_const_gen var (fun _ x => x) t.
 
-  Definition InlineConst {t} (e : Expr t) : Expr t
-    := fun var => inline_const (e _).
+  Definition InlineConstGen (postprocess : forall var t, @exprf var t -> @exprf var t)
+             {t} (e : Expr t) : Expr t
+    := fun var => inline_const_gen (postprocess _) (e _).
+  Definition InlineConst {t} := @InlineConstGen (fun _ _ x => x) t.
 End language.
 
+Global Arguments inline_const_genf {_ _ _ _} postprocess {_} _.
+Global Arguments inline_const_gen {_ _ _ _} postprocess {_} _.
+Global Arguments InlineConstGen {_ _ _} postprocess {_} _ var.
 Global Arguments inline_constf {_ _ _ _ _} _.
 Global Arguments inline_const {_ _ _ _ _} _.
 Global Arguments InlineConst {_ _ _ _} _ var.