Add reflective compose, notation for Z.Syntax.{Expr,Interp}

26 files changed, 92 insertions, 72 deletions

diff --git a/src/Compilers/ExprInversion.v b/src/Compilers/ExprInversion.v
index 48ea30907..4820b5f39 100644
--- a/src/Compilers/ExprInversion.v
+++ b/src/Compilers/ExprInversion.v
@@ -54,6 +54,11 @@ Section language.
     Definition invert_Abs {T} (e : expr T) : interp_flat_type_gen var (domain T) -> exprf (codomain T)
       := match e with Abs _ _ f => f end.
 
+    Definition compose {A B C} (f : expr (B -> C)) (g : expr (A -> B))
+      : expr (A -> C)
+      := Abs (fun v => LetIn (invert_Abs g v)
+                             (invert_Abs f)).
+
     Definition exprf_code {t} (e : exprf t) : exprf t -> Prop
       := match e with
          | TT => fun e' => TT = e'
@@ -148,6 +153,10 @@ Section language.
     : Syntax.interpf interp_op (@invert_Abs interp_base_type T e x)
       = Syntax.interp interp_op e x.
   Proof using Type. destruct e; reflexivity. Qed.
+
+  Definition Compose {A B C} (f : Expr (B -> C)) (g : Expr (A -> B))
+    : Expr (A -> C)
+    := fun var => compose (f var) (g var).
 End language.
 
 Global Arguments invert_Var {_ _ _ _} _.
@@ -156,6 +165,12 @@ Global Arguments invert_LetIn {_ _ _ _} _.
 Global Arguments invert_Pair {_ _ _ _ _} _.
 Global Arguments invert_Abs {_ _ _ _} _ _.
 
+Module Export Notations.
+  Infix "∘" := Compose : expr_scope.
+  Infix "∘f" := compose : expr_scope.
+  Infix "∘ᶠ" := compose : expr_scope.
+End Notations.
+
 Ltac invert_one_expr e :=
   preinvert_one_type e;
   intros ? e;
diff --git a/src/Compilers/Syntax.v b/src/Compilers/Syntax.v
index 0e8f924da..c86567c6d 100644
--- a/src/Compilers/Syntax.v
+++ b/src/Compilers/Syntax.v
@@ -148,6 +148,7 @@ Module Export Notations.
   Notation "( x , y , .. , z )" := (Pair .. (Pair x%expr y%expr) .. z%expr) : expr_scope.
   Notation "( )" := TT : expr_scope.
   Notation "()" := TT : expr_scope.
+  Infix "^" := (@tuple _) : ctype_scope.
   Bind Scope ctype_scope with flat_type.
   Bind Scope ctype_scope with type.
 End Notations.
diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v
index 6cb922129..5a5b95a22 100644
--- a/src/Compilers/Z/ArithmeticSimplifier.v
+++ b/src/Compilers/Z/ArithmeticSimplifier.v
@@ -10,7 +10,6 @@ Require Import Crypto.Util.ZUtil.Definitions.
 Section language.
   Context (convert_adc_to_sbb : bool).
   Local Notation exprf := (@exprf base_type op).
-  Local Notation Expr := (@Expr base_type op).
 
   Section with_var.
     Context {var : base_type -> Type}.
diff --git a/src/Compilers/Z/ArithmeticSimplifierInterp.v b/src/Compilers/Z/ArithmeticSimplifierInterp.v
index b55f069e1..cd76a3479 100644
--- a/src/Compilers/Z/ArithmeticSimplifierInterp.v
+++ b/src/Compilers/Z/ArithmeticSimplifierInterp.v
@@ -22,7 +22,6 @@ Require Import Crypto.Util.Tactics.UniquePose.
 
 Local Notation exprf := (@exprf base_type op interp_base_type).
 Local Notation expr := (@expr base_type op interp_base_type).
-Local Notation Expr := (@Expr base_type op).
 
 Local Ltac fin_t :=
   first [ exact I
@@ -103,7 +102,7 @@ Local Arguments lift_op / .
 Local Opaque Z.pow.
 
 Lemma InterpSimplifyArith {convert_adc_to_sbb} {t} (e : Expr t)
-  : forall x, Interp interp_op (SimplifyArith convert_adc_to_sbb e) x = Interp interp_op e x.
+  : forall x, Interp (SimplifyArith convert_adc_to_sbb e) x = Interp e x.
 Proof.
   apply InterpRewriteOp; intros; unfold simplify_op_expr.
   Time break_innermost_match;
diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v
index 33f3c3335..ff690688a 100644
--- a/src/Compilers/Z/ArithmeticSimplifierWf.v
+++ b/src/Compilers/Z/ArithmeticSimplifierWf.v
@@ -21,7 +21,6 @@ Require Import Crypto.Util.HProp.
 
 Local Notation exprf := (@exprf base_type op).
 Local Notation expr := (@expr base_type op).
-Local Notation Expr := (@Expr base_type op).
 Local Notation wff := (@wff base_type op).
 Local Notation Wf := (@Wf base_type op).
 
diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v
index dc557f6ec..25762401d 100644
--- a/src/Compilers/Z/Bounds/Interpretation.v
+++ b/src/Compilers/Z/Bounds/Interpretation.v
@@ -1,6 +1,6 @@
 Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Compilers.Z.Syntax.
 Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Z.Syntax.
 Require Import Crypto.Compilers.Relations.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Decidable.
@@ -285,10 +285,10 @@ Module Import Bounds.
     := let good_lgsz := List.filter (Nat.leb lgsz) allowable_lgsz in
        List.fold_right (fun a b => Some (option_min a b)) None good_lgsz.
 
-  Definition ComputeBounds {t} (e : Expr base_type op t)
+  Definition ComputeBounds {t} (e : Expr t)
              (input_bounds : interp_flat_type interp_base_type (domain t))
     : interp_flat_type interp_base_type (codomain t)
-    := Interp (@interp_op) e input_bounds.
+    := Compilers.Syntax.Interp (@interp_op) e input_bounds.
 
   Definition is_tighter_thanb' {T} : interp_base_type T -> interp_base_type T -> bool
     := is_tighter_than_bool.
diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v
index 28e305a8f..1217cd721 100644
--- a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v
+++ b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v
@@ -14,15 +14,15 @@ Require Import Crypto.Util.PointedProp.
 
 Lemma MapCastCorrect
       {round_up}
-      {t} (e : Expr base_type op t)
+      {t} (e : Expr t)
       (Hwf : Wf e)
       (input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
   : forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e'))
            v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v)
            (Hside : to_prop (InterpSideConditions e v)),
-    Interp (@Bounds.interp_op) e input_bounds = b
-    /\ Bounds.is_bounded_by b (Interp interp_op e v)
-    /\ cast_back_flat_const (Interp interp_op e' v') = (Interp interp_op e v).
+    Compilers.Syntax.Interp (@Bounds.interp_op) e input_bounds = b
+    /\ Bounds.is_bounded_by b (Compilers.Syntax.Interp interp_op e v)
+    /\ cast_back_flat_const (Compilers.Syntax.Interp interp_op e' v') = (Compilers.Syntax.Interp interp_op e v).
 Proof.
   apply MapCastCorrect; auto.
   { apply is_bounded_by_interp_op. }
@@ -31,18 +31,18 @@ Qed.
 
 Lemma MapCastCorrect_eq
       {round_up}
-      {t} (e : Expr base_type op t)
+      {t} (e : Expr t)
       {evb ev}
       (Hwf : Wf e)
       (input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
   : forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e'))
            v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v)
            (Hside : to_prop (InterpSideConditions e v))
-           (Hevb : evb = Interp (@Bounds.interp_op) e input_bounds)
-           (Hev : ev = Interp interp_op e v),
+           (Hevb : evb = Compilers.Syntax.Interp (@Bounds.interp_op) e input_bounds)
+           (Hev : ev = Compilers.Syntax.Interp interp_op e v),
     evb = b
     /\ Bounds.is_bounded_by b ev
-    /\ cast_back_flat_const (Interp interp_op e' v') = ev.
+    /\ cast_back_flat_const (Compilers.Syntax.Interp interp_op e' v') = ev.
 Proof.
   intros; subst; apply MapCastCorrect; auto.
 Qed.
diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v
index 7432b752b..fabb8b2b8 100644
--- a/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v
+++ b/src/Compilers/Z/Bounds/MapCastByDeBruijnWf.v
@@ -10,7 +10,7 @@ Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn.
 
 Definition Wf_MapCast
            {round_up}
-           {t} (e : Expr base_type op t)
+           {t} (e : Expr t)
            (input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
            {b} e' (He' : MapCast round_up e input_bounds = Some (existT _ b e'))
            (Hwf : Wf e)
@@ -23,7 +23,7 @@ Definition Wf_MapCast
 
 Definition Wf_MapCast_arrow
            {round_up}
-           {s d} (e : Expr base_type op (Arrow s d))
+           {s d} (e : Expr (Arrow s d))
            (input_bounds : interp_flat_type Bounds.interp_base_type s)
            {b} e' (He' : MapCast round_up e input_bounds = Some (existT _ b e'))
            (Hwf : Wf e)
diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v
index c4973debf..34cb7a47a 100644
--- a/src/Compilers/Z/Bounds/Pipeline/Definition.v
+++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v
@@ -33,7 +33,7 @@ Require Import Crypto.Compilers.Z.ArithmeticSimplifierInterp.
 
 (** *** Definition of the Pre-Wf Pipeline *)
 (** Do not change the name or the type of this definition *)
-Definition PreWfPipeline {t} (e : Expr base_type op t) : Expr base_type op _
+Definition PreWfPipeline {t} (e : Expr t) : Expr _
   := ExprEta (SimplifyArith false (Linearize e)).
 
 (** *** Correctness proof of the Pre-Wf Pipeline *)
@@ -41,8 +41,8 @@ Definition PreWfPipeline {t} (e : Expr base_type op t) : Expr base_type op _
     change it's proof, either; all of the relevant lemmas should be in
     the [reflective_interp] rewrite database.  If they're not, you
     should find the file where they are defined and add them. *)
-Lemma InterpPreWfPipeline {t} (e : Expr base_type op t)
-  : forall x, Interp interp_op (PreWfPipeline e) x = Interp interp_op e x.
+Lemma InterpPreWfPipeline {t} (e : Expr t)
+  : forall x, Interp (PreWfPipeline e) x = Interp e x.
 Proof.
   unfold PreWfPipeline; intro.
   repeat autorewrite with reflective_interp.
@@ -86,8 +86,8 @@ Definition default_PipelineOptions :=
     the expression. *)
 Definition PostWfPreBoundsPipeline
            (opts : PipelineOptions)
-           {t} (e : Expr base_type op t)
-  : Expr base_type op t
+           {t} (e : Expr t)
+  : Expr t
   := let e := InlineConst e in
      let e := InlineConst (Linearize (SimplifyArith false e)) in
      let e := InlineConst (Linearize (SimplifyArith false e)) in
@@ -117,8 +117,8 @@ Definition PostWfPreBoundsPipeline
 Definition PostWfBoundsPipeline
            round_up
            (opts : PipelineOptions)
-           {t} (e0 : Expr base_type op t)
-           (e : Expr base_type op t)
+           {t} (e0 : Expr t)
+           (e : Expr t)
            (input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
   : option (@ProcessedReflectivePackage round_up)
   := Build_ProcessedReflectivePackage_from_option_sigma
@@ -167,7 +167,7 @@ Section with_round_up_list.
   Definition PostWfPipelineCorrect
              opts
              {t}
-             (e : Expr base_type op t)
+             (e : Expr t)
              (input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
              (Hwf : Wf e)
              (e' := PostWfPreBoundsPipeline opts e)
@@ -177,8 +177,8 @@ Section with_round_up_list.
              (v' : interp_flat_type Syntax.interp_base_type (pick_type input_bounds))
              (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v)
              (Hside : to_prop (InterpSideConditions e' v))
-    : Bounds.is_bounded_by b (Interp interp_op e v)
-      /\ cast_back_flat_const (Interp interp_op e'' v') = Interp interp_op e v.
+    : Bounds.is_bounded_by b (Interp e v)
+      /\ cast_back_flat_const (Interp e'' v') = Interp e v.
   Proof using Type.
     (** These first two lines probably shouldn't change much *)
     unfold PostWfBoundsPipeline, PostWfPreBoundsPipeline, Build_ProcessedReflectivePackage_from_option_sigma, option_map, projT2_map in *; subst e'.
diff --git a/src/Compilers/Z/Bounds/Pipeline/OutputType.v b/src/Compilers/Z/Bounds/Pipeline/OutputType.v
index 88e38fbf6..028dd23a9 100644
--- a/src/Compilers/Z/Bounds/Pipeline/OutputType.v
+++ b/src/Compilers/Z/Bounds/Pipeline/OutputType.v
@@ -16,16 +16,16 @@ Section with_round_up_list.
 
   Record ProcessedReflectivePackage
     := { InputType : _;
-         input_expr : Expr base_type op InputType;
+         input_expr : Expr InputType;
          input_bounds : interp_flat_type Bounds.interp_base_type (domain InputType);
          output_bounds :> interp_flat_type Bounds.interp_base_type (codomain InputType);
-         output_expr :> Expr base_type op (Arrow (pick_type input_bounds) (pick_type output_bounds)) }.
+         output_expr :> Expr (Arrow (pick_type input_bounds) (pick_type output_bounds)) }.
 
   Definition Build_ProcessedReflectivePackage_from_option_sigma
-             {t} (e : Expr base_type op t)
+             {t} (e : Expr t)
              (input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
              (result : option { output_bounds : interp_flat_type Bounds.interp_base_type (codomain t)
-                                                & Expr base_type op (Arrow (pick_type input_bounds) (pick_type output_bounds)) })
+                                                & Expr (Arrow (pick_type input_bounds) (pick_type output_bounds)) })
     : option ProcessedReflectivePackage
     := option_map
          (fun be
@@ -35,10 +35,10 @@ Section with_round_up_list.
 
   Definition ProcessedReflectivePackage_to_sigT (x : ProcessedReflectivePackage)
     : { InputType : _
-                    & Expr base_type op InputType
+                    & Expr InputType
                       * { bounds : interp_flat_type Bounds.interp_base_type (domain InputType)
                                    * interp_flat_type Bounds.interp_base_type (codomain InputType)
-                                   & Expr base_type op (Arrow (pick_type (fst bounds)) (pick_type (snd bounds))) } }%type
+                                   & Expr (Arrow (pick_type (fst bounds)) (pick_type (snd bounds))) } }%type
     := let (a, b, c, d, e) := x in
        existT _ a (b, (existT _ (c, d) e)).
 End with_round_up_list.
diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
index 9194f49db..a4b289c8e 100644
--- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
+++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v
@@ -212,7 +212,7 @@ Section with_round_up_list.
              {e_pre_pkg}
              {e_pkg}
              (** ** reification *)
-             (rexpr_sig : { rexpr : Expr base_type op t | forall x, Interp Syntax.interp_op rexpr x = fZ x })
+             (rexpr_sig : { rexpr : Expr t | forall x, Interp rexpr x = fZ x })
              (** ** pre-wf pipeline *)
              (He : e = PreWfPipeline (proj1_sig rexpr_sig))
              (** ** proving wf *)
@@ -232,7 +232,7 @@ Section with_round_up_list.
              (Hbounds_sane : pick_type given_output_bounds = pick_type b)
              (Hbounds_sane_refl
               : e_final_newtype
-                = eq_rect _ (fun t => Expr base_type op (Arrow (pick_type input_bounds) t)) e' _ (eq_sym Hbounds_sane))
+                = eq_rect _ (fun t => Expr (Arrow (pick_type input_bounds) t)) e' _ (eq_sym Hbounds_sane))
              (** ** instantiation of original evar *)
              (Hevar : final_e_evar = InterpEta (t:=Arrow _ _) Syntax.interp_op e_final_newtype v')
              (** ** side conditions (boundedness) *)
@@ -255,8 +255,8 @@ Section with_round_up_list.
     rewrite !@InterpPreWfPipeline in Hpost_correct.
     unshelve eapply relax_output_bounds; try eassumption; [].
     match goal with
-    | [ |- context[Interp _ (@eq_rect ?A ?x ?P ?k ?y ?pf) ?v] ]
-      => rewrite (@ap_transport A P _ x y pf (fun t e => Interp interp_op e v) k)
+    | [ |- context[Interp (@eq_rect ?A ?x ?P ?k ?y ?pf) ?v] ]
+      => rewrite (@ap_transport A P _ x y pf (fun t e => Interp e v) k)
     end.
     rewrite <- transport_pp, concat_Vp; simpl.
     apply Hpost_correct.
diff --git a/src/Compilers/Z/CommonSubexpressionElimination.v b/src/Compilers/Z/CommonSubexpressionElimination.v
index c2b4775c6..2493f6041 100644
--- a/src/Compilers/Z/CommonSubexpressionElimination.v
+++ b/src/Compilers/Z/CommonSubexpressionElimination.v
@@ -218,13 +218,13 @@ Definition cse inline_symbolic_expr_in_lookup {var} (prefix : list _) {t} (v : e
           normalize_symbolic_expr_mod_c
           inline_symbolic_expr_in_lookup var prefix t v xs.
 
-Definition CSE_gen inline_symbolic_expr_in_lookup {t} (e : Expr _ _ t) (prefix : forall var, list { t : flat_type base_type & exprf _ _ t })
-  : Expr _ _ t
+Definition CSE_gen inline_symbolic_expr_in_lookup {t} (e : Expr t) (prefix : forall var, list { t : flat_type base_type & exprf _ _ t })
+  : Expr t
   := @CSE base_type symbolic_op base_type_beq symbolic_op_beq
           internal_base_type_dec_bl op symbolize_op
           normalize_symbolic_expr_mod_c
           inline_symbolic_expr_in_lookup t e prefix.
 
-Definition CSE inline_symbolic_expr_in_lookup {t} (e : Expr _ _ t)
-  : Expr _ _ t
+Definition CSE inline_symbolic_expr_in_lookup {t} (e : Expr t)
+  : Expr t
   := @CSE_gen inline_symbolic_expr_in_lookup t e (fun _ => nil).
diff --git a/src/Compilers/Z/CommonSubexpressionEliminationInterp.v b/src/Compilers/Z/CommonSubexpressionEliminationInterp.v
index 280039058..7e7f7910a 100644
--- a/src/Compilers/Z/CommonSubexpressionEliminationInterp.v
+++ b/src/Compilers/Z/CommonSubexpressionEliminationInterp.v
@@ -6,16 +6,16 @@ Require Import Crypto.Compilers.Z.Syntax.
 Require Import Crypto.Compilers.CommonSubexpressionEliminationInterp.
 Require Import Crypto.Compilers.Z.CommonSubexpressionElimination.
 
-Lemma InterpCSE_gen inline_symbolic_expr_in_lookup t (e : Expr _ _ t) prefix
+Lemma InterpCSE_gen inline_symbolic_expr_in_lookup t (e : Expr t) prefix
       (Hwf : Wf e)
-  : forall x, Interp interp_op (@CSE_gen inline_symbolic_expr_in_lookup t e prefix) x = Interp interp_op e x.
+  : forall x, Interp (@CSE_gen inline_symbolic_expr_in_lookup t e prefix) x = Interp e x.
 Proof.
   apply InterpCSE;
     auto using internal_base_type_dec_bl, internal_base_type_dec_lb, internal_symbolic_op_dec_bl, internal_symbolic_op_dec_lb, denote_symbolic_op.
 Qed.
 
-Lemma InterpCSE inline_symbolic_expr_in_lookup t (e : Expr _ _ t) (Hwf : Wf e)
-  : forall x, Interp interp_op (@CSE inline_symbolic_expr_in_lookup t e) x = Interp interp_op e x.
+Lemma InterpCSE inline_symbolic_expr_in_lookup t (e : Expr t) (Hwf : Wf e)
+  : forall x, Interp (@CSE inline_symbolic_expr_in_lookup t e) x = Interp e x.
 Proof.
   apply InterpCSE_gen; auto.
 Qed.
diff --git a/src/Compilers/Z/CommonSubexpressionEliminationWf.v b/src/Compilers/Z/CommonSubexpressionEliminationWf.v
index a7365397c..93d422b2d 100644
--- a/src/Compilers/Z/CommonSubexpressionEliminationWf.v
+++ b/src/Compilers/Z/CommonSubexpressionEliminationWf.v
@@ -5,7 +5,7 @@ Require Import Crypto.Compilers.Z.Syntax.
 Require Import Crypto.Compilers.CommonSubexpressionEliminationWf.
 Require Import Crypto.Compilers.Z.CommonSubexpressionElimination.
 
-Lemma Wf_CSE_gen inline_symbolic_expr_in_lookup t (e : Expr _ _ t)
+Lemma Wf_CSE_gen inline_symbolic_expr_in_lookup t (e : Expr t)
       prefix
       (Hlen : forall var1 var2, length (prefix var1) = length (prefix var2))
       (Hprefix : forall var1 var2 n t1 t2 e1 e2,
@@ -18,7 +18,7 @@ Proof.
   apply Wf_CSE; auto using internal_base_type_dec_bl, internal_base_type_dec_lb, internal_symbolic_op_dec_bl, internal_symbolic_op_dec_lb.
 Qed.
 
-Lemma Wf_CSE inline_symbolic_expr_in_lookup t (e : Expr _ _ t)
+Lemma Wf_CSE inline_symbolic_expr_in_lookup t (e : Expr t)
       (Hwf : Wf e)
   : Wf (@CSE inline_symbolic_expr_in_lookup t e).
 Proof.
diff --git a/src/Compilers/Z/FoldTypes.v b/src/Compilers/Z/FoldTypes.v
index fc6aa9406..7b3059e43 100644
--- a/src/Compilers/Z/FoldTypes.v
+++ b/src/Compilers/Z/FoldTypes.v
@@ -7,11 +7,11 @@ Section min_or_max.
   Context (f : base_type -> base_type -> base_type)
           (init : base_type).
 
-  Definition TypeFold {t} (e : Expr base_type op t) : base_type
+  Definition TypeFold {t} (e : Expr t) : base_type
     := TypeFold (fun t => t) f init e.
 End min_or_max.
 
-Definition MaxTypeUsed {t} (e : Expr base_type op t) : base_type
+Definition MaxTypeUsed {t} (e : Expr t) : base_type
   := TypeFold base_type_max (TWord 0) e.
-Definition MinTypeUsed {t} (e : Expr base_type op t) : base_type
+Definition MinTypeUsed {t} (e : Expr t) : base_type
   := TypeFold base_type_min TZ e.
diff --git a/src/Compilers/Z/Inline.v b/src/Compilers/Z/Inline.v
index df46c0ecf..cbe6dbfde 100644
--- a/src/Compilers/Z/Inline.v
+++ b/src/Compilers/Z/Inline.v
@@ -3,8 +3,8 @@ Require Import Crypto.Compilers.Inline.
 Require Import Crypto.Compilers.Z.Syntax.
 Require Import Crypto.Compilers.Z.Syntax.Util.
 
-Definition InlineConstAndOpp {t} (e : Expr base_type op t) : Expr base_type op t
+Definition InlineConstAndOpp {t} (e : Expr t) : Expr t
   := @InlineConst base_type op (is_const_or_opp) t e.
 
-Definition InlineConst {t} (e : Expr base_type op t) : Expr base_type op t
+Definition InlineConst {t} (e : Expr t) : Expr t
   := @InlineConst base_type op (is_const) t e.
diff --git a/src/Compilers/Z/InlineInterp.v b/src/Compilers/Z/InlineInterp.v
index 46e5064e9..6413a68cd 100644
--- a/src/Compilers/Z/InlineInterp.v
+++ b/src/Compilers/Z/InlineInterp.v
@@ -4,12 +4,12 @@ Require Import Crypto.Compilers.InlineInterp.
 Require Import Crypto.Compilers.Z.Syntax.
 Require Import Crypto.Compilers.Z.Inline.
 
-Definition InterpInlineConstAndOpp {interp_base_type interp_op} {t} (e : Expr base_type op t) (Hwf : Wf e)
-  : forall x, Interp interp_op (InlineConstAndOpp e) x = Interp interp_op e x
+Definition InterpInlineConstAndOpp {interp_base_type interp_op} {t} (e : Expr t) (Hwf : Wf e)
+  : forall x, Compilers.Syntax.Interp interp_op (InlineConstAndOpp e) x = Compilers.Syntax.Interp interp_op e x
   := @InterpInlineConst _ interp_base_type _ _ _ t e Hwf.
 
-Definition InterpInlineConst {interp_base_type interp_op} {t} (e : Expr base_type op t) (Hwf : Wf e)
-  : forall x, Interp interp_op (InlineConst e) x = Interp interp_op e x
+Definition InterpInlineConst {interp_base_type interp_op} {t} (e : Expr t) (Hwf : Wf e)
+  : forall x, Compilers.Syntax.Interp interp_op (InlineConst e) x = Compilers.Syntax.Interp interp_op e x
   := @InterpInlineConst _ interp_base_type _ _ _ t e Hwf.
 
 Hint Rewrite @InterpInlineConstAndOpp @InterpInlineConst using solve_wf_side_condition : reflective_interp.
diff --git a/src/Compilers/Z/InlineWf.v b/src/Compilers/Z/InlineWf.v
index d6b846460..b7726987b 100644
--- a/src/Compilers/Z/InlineWf.v
+++ b/src/Compilers/Z/InlineWf.v
@@ -4,11 +4,11 @@ Require Import Crypto.Compilers.InlineWf.
 Require Import Crypto.Compilers.Z.Syntax.
 Require Import Crypto.Compilers.Z.Inline.
 
-Definition Wf_InlineConstAndOpp {t} (e : Expr base_type op t) (Hwf : Wf e)
+Definition Wf_InlineConstAndOpp {t} (e : Expr t) (Hwf : Wf e)
   : Wf (InlineConstAndOpp e)
   := @Wf_InlineConst _ _ _ t e Hwf.
 
-Definition Wf_InlineConst {t} (e : Expr base_type op t) (Hwf : Wf e)
+Definition Wf_InlineConst {t} (e : Expr t) (Hwf : Wf e)
   : Wf (InlineConst e)
   := @Wf_InlineConst _ _ _ t e Hwf.
 
diff --git a/src/Compilers/Z/InterpSideConditions.v b/src/Compilers/Z/InterpSideConditions.v
index 7429eaba7..bc3c8f6a9 100644
--- a/src/Compilers/Z/InterpSideConditions.v
+++ b/src/Compilers/Z/InterpSideConditions.v
@@ -5,5 +5,5 @@ Require Import Crypto.Compilers.InterpSideConditions.
 Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Notations.
 
-Definition InterpSideConditions {t} (e : Expr base_type op t) : interp_flat_type interp_base_type (domain t) -> pointed_Prop
+Definition InterpSideConditions {t} (e : Expr t) : interp_flat_type interp_base_type (domain t) -> pointed_Prop
     := InterpSideConditions interp_op (@interped_op_side_conditions) e.
diff --git a/src/Compilers/Z/MapCastByDeBruijnInterp.v b/src/Compilers/Z/MapCastByDeBruijnInterp.v
index 068c74ef2..0103342f4 100644
--- a/src/Compilers/Z/MapCastByDeBruijnInterp.v
+++ b/src/Compilers/Z/MapCastByDeBruijnInterp.v
@@ -41,15 +41,15 @@ Section language.
     := (@MapCast interp_base_type_bounds interp_op_bounds pick_typeb cast_op).
 
   Lemma MapCastCorrect
-        {t} (e : Expr base_type op t)
+        {t} (e : Expr t)
         (Hwf : Wf e)
         (input_bounds : interp_flat_type interp_base_type_bounds (domain t))
     : forall {b} e' (He':MapCast e input_bounds = Some (existT _ b e'))
              v v' (Hv : @inbounds _ input_bounds v /\ cast_back _ _ v' = v)
              (Hside : to_prop (InterpSideConditions e v)),
-      Interp interp_op_bounds e input_bounds = b
-      /\ @inbounds _ b (Interp interp_op e v)
-      /\ cast_back _ _ (Interp interp_op e' v') = (Interp interp_op e v).
+      Compilers.Syntax.Interp interp_op_bounds e input_bounds = b
+      /\ @inbounds _ b (Compilers.Syntax.Interp interp_op e v)
+      /\ cast_back _ _ (Compilers.Syntax.Interp interp_op e' v') = (Compilers.Syntax.Interp interp_op e v).
   Proof using Type*.
     apply MapCastCorrect; auto using internal_base_type_dec_lb.
   Qed.
diff --git a/src/Compilers/Z/MapCastByDeBruijnWf.v b/src/Compilers/Z/MapCastByDeBruijnWf.v
index cce16e5fe..791e33886 100644
--- a/src/Compilers/Z/MapCastByDeBruijnWf.v
+++ b/src/Compilers/Z/MapCastByDeBruijnWf.v
@@ -36,7 +36,7 @@ Section language.
     := (@MapCast interp_base_type_bounds interp_op_bounds pick_typeb cast_op).
 
   Definition Wf_MapCast
-             {t} (e : Expr base_type op t)
+             {t} (e : Expr t)
              (input_bounds : interp_flat_type interp_base_type_bounds (domain t))
              {b} e' (He' : MapCast e input_bounds = Some (existT _ b e'))
              (Hwf : Wf e)
@@ -45,7 +45,7 @@ Section language.
          _ _ _ internal_base_type_dec_bl internal_base_type_dec_lb _ _ _ _ _
          t e input_bounds b e' He' Hwf.
   Definition Wf_MapCast_arrow
-             {s d} (e : Expr base_type op (Arrow s d))
+             {s d} (e : Expr (Arrow s d))
              (input_bounds : interp_flat_type interp_base_type_bounds s)
              {b} e' (He' : MapCast e input_bounds = Some (existT _ b e'))
              (Hwf : Wf e)
diff --git a/src/Compilers/Z/RewriteAddToAdc.v b/src/Compilers/Z/RewriteAddToAdc.v
index 5f3fc05c5..838c92b75 100644
--- a/src/Compilers/Z/RewriteAddToAdc.v
+++ b/src/Compilers/Z/RewriteAddToAdc.v
@@ -24,8 +24,8 @@ Local Open Scope bool_scope.
 Section language.
   Local Notation PContext var := (PositiveContext _ var _ internal_base_type_dec_bl).
 
-  Definition RewriteAdc {t} (e : Expr base_type op t)
-    : Expr base_type op t
+  Definition RewriteAdc {t} (e : Expr t)
+    : Expr t
     := let is_good e' := match option_map (wf_unit (Context:=PContext _) empty) e' with
                          | Some (Some trivial) => true
                          | _ => false
@@ -49,7 +49,7 @@ Section language.
        then let e' := option_map interp_to_phoas e' in
             match e' with
             | Some e'
-              => match t return Expr _ _ (Arrow (domain t) (codomain t)) -> Expr _ _ t with
+              => match t return Expr (Arrow (domain t) (codomain t)) -> Expr t with
                  | Arrow _ _ => fun x => x
                  end e'
             | None => e
diff --git a/src/Compilers/Z/RewriteAddToAdcInterp.v b/src/Compilers/Z/RewriteAddToAdcInterp.v
index 0fdb2e46c..28953a3fb 100644
--- a/src/Compilers/Z/RewriteAddToAdcInterp.v
+++ b/src/Compilers/Z/RewriteAddToAdcInterp.v
@@ -20,8 +20,8 @@ Section language.
   Local Notation PContext var := (PositiveContext _ var _ internal_base_type_dec_bl).
 
   Lemma InterpRewriteAdc
-        {t} (e : Expr base_type op t) (Hwf : Wf e)
-  : forall x, Interp interp_op (RewriteAdc e) x = Interp interp_op e x.
+        {t} (e : Expr t) (Hwf : Wf e)
+  : forall x, Compilers.Syntax.Interp interp_op (RewriteAdc e) x = Compilers.Syntax.Interp interp_op e x.
   Proof.
     intro x; unfold RewriteAdc, option_map; break_innermost_match; try reflexivity;
       match goal with |- ?x = ?y => cut (Some x = Some y); [ congruence | ] end;
@@ -39,7 +39,7 @@ Section language.
                   => let lhs := match goal with |- ?lhs = _ => lhs end in
                      let H := fresh in
                      destruct lhs eqn:H; [ apply (f_equal (@Some _)); eapply @Interp_rewrite_expr in H | ]
-                | [ H : Compile.compile (?e _) _ = Some ?e'', H' : Syntax.Named.Interp ?e'' ?x = Some ?v' |- ?v' = Interp ?interp_op' ?e ?x ]
+                | [ H : Compile.compile (?e _) _ = Some ?e'', H' : Syntax.Named.Interp ?e'' ?x = Some ?v' |- ?v' = Compilers.Syntax.Interp ?interp_op' ?e ?x ]
                   => eapply @Interp_compile with (v:=x) (interp_op:=interp_op') in H
                 end
               | intros; exact (@PositiveContextOk _ _ base_type_beq internal_base_type_dec_bl internal_base_type_dec_lb)
diff --git a/src/Compilers/Z/RewriteAddToAdcWf.v b/src/Compilers/Z/RewriteAddToAdcWf.v
index cabe61b03..984d2a3e1 100644
--- a/src/Compilers/Z/RewriteAddToAdcWf.v
+++ b/src/Compilers/Z/RewriteAddToAdcWf.v
@@ -13,7 +13,7 @@ Require Import Crypto.Util.Bool.
 Section language.
   Local Hint Resolve internal_base_type_dec_lb internal_base_type_dec_lb dec_rel_of_bool_dec_rel : typeclass_instances.
 
-  Lemma Wf_RewriteAdc {t} (e : Expr base_type op t) (Hwf : Wf e)
+  Lemma Wf_RewriteAdc {t} (e : Expr t) (Hwf : Wf e)
   : Wf (RewriteAdc e).
   Proof.
     unfold RewriteAdc, option_map; break_innermost_match;
diff --git a/src/Compilers/Z/Syntax.v b/src/Compilers/Z/Syntax.v
index 818fa1ad5..de4626adb 100644
--- a/src/Compilers/Z/Syntax.v
+++ b/src/Compilers/Z/Syntax.v
@@ -98,3 +98,6 @@ Definition Zinterp_op src dst (f : op src dst)
 
 Definition interp_op src dst (f : op src dst) : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst
   := lift_op (Zinterp_op src dst f).
+
+Notation Expr := (Expr base_type op).
+Notation Interp := (Interp interp_op).
diff --git a/src/Util/Notations.v b/src/Util/Notations.v
index 5581dcbc4..206b25d9c 100644
--- a/src/Util/Notations.v
+++ b/src/Util/Notations.v
@@ -10,6 +10,10 @@ Require Export Crypto.Util.GlobalSettings.
 
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "()" (at level 0).
+Reserved Infix "∘" (at level 40, left associativity).
+Reserved Infix "∘ᶠ" (at level 40, left associativity).
+Reserved Infix "∘f" (at level 40, left associativity).
+Reserved Infix "'o'" (at level 40, left associativity).
 Reserved Infix "=?" (at level 70, no associativity).
 Reserved Infix "<?" (at level 70, no associativity).
 Reserved Infix "<=?" (at level 70, no associativity).