Make use of named syntax, do reg assign for fancy

1 files changed, 178 insertions, 201 deletions

diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v
index 2392f7ede..440f1aa4f 100644
--- a/src/Specific/FancyMachine256/Core.v
+++ b/src/Specific/FancyMachine256/Core.v
@@ -1,11 +1,17 @@
 (** * A Fancy Machine with 256-bit registers *)
 Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms.
-Require Export Coq.ZArith.ZArith.
+Require Import Coq.PArith.BinPos Coq.micromega.Psatz.
+Require Export Coq.ZArith.ZArith Coq.Lists.List.
+Require Import Crypto.Util.Decidable.
 Require Export Crypto.BoundedArithmetic.Interface.
 Require Export Crypto.BoundedArithmetic.ArchitectureToZLike.
 Require Export Crypto.BoundedArithmetic.ArchitectureToZLikeProofs.
 Require Export Crypto.Util.Tuple.
 Require Import Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod.
+Require Export Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Reflection.Named.DeadCodeElimination.
+Require Import Crypto.Reflection.CountLets.
+Require Import Crypto.Reflection.Named.ContextOn.
 Require Export Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Linearize.
 Require Import Crypto.Reflection.Inline.
@@ -13,6 +19,8 @@ Require Import Crypto.Reflection.CommonSubexpressionElimination.
 Require Export Crypto.Reflection.Reify.
 Require Export Crypto.Util.ZUtil.
 Require Export Crypto.Util.Notations.
+Require Import Crypto.Util.ListUtil.
+Export ListNotations.
 
 Open Scope Z_scope.
 Local Notation eta x := (fst x, snd x).
@@ -25,6 +33,8 @@ Section reflection.
   Local Set Boolean Equality Schemes.
   Local Set Decidable Equality Schemes.
   Inductive base_type := TZ | Tbool | TW.
+  Global Instance dec_base_type : DecidableRel (@eq base_type)
+    := base_type_eq_dec.
   Definition interp_base_type (v : base_type) : Type :=
     match v with
     | TZ => Z
@@ -94,6 +104,27 @@ Section reflection.
        end.
 
   Definition CSE {t} e := @CSE base_type SConstT op_code base_type_beq SConstT_beq op_code_beq internal_base_type_dec_bl interp_base_type op symbolicify_const symbolicify_op t e (fun _ => nil).
+
+  Inductive inline_option := opt_inline | opt_default | opt_noinline.
+
+  Definition postprocess var t (e : @exprf base_type interp_base_type op var t)
+    : @inline_directive base_type interp_base_type op var t
+    := let opt : inline_option
+           := match e with
+              | Op _ _ OPshl _ => opt_inline
+              | Op _ _ OPshr _ => opt_inline
+              | _ => opt_default
+              end in
+       match opt with
+       | opt_noinline => no_inline e
+       | opt_default => default_inline e
+       | opt_inline => match t as t' return exprf _ _ _ t' -> inline_directive t' with
+                       | Tbase _ => fun e => inline e
+                       | _ => fun e => default_inline e
+                       end e
+       end.
+
+  Definition Inline {t} e := @InlineConstGen base_type interp_base_type op postprocess t e.
 End reflection.
 
 Ltac base_reify_op op op_head ::=
@@ -121,7 +152,7 @@ Ltac base_reify_type T ::=
 Ltac Reify' e := Reify.Reify' base_type (interp_base_type _) op e.
 Ltac Reify e :=
   let v := Reify.Reify base_type (interp_base_type _) op e in
-  constr:(CSE _ (InlineConst (Linearize v))).
+  constr:(Inline _ (CSE _ (InlineConst (Linearize v)))).
 (*Ltac Reify_rhs := Reify.Reify_rhs base_type (interp_base_type _) op (interp_op _).*)
 
 (** ** Raw Syntax Trees *)
@@ -132,226 +163,172 @@ Ltac Reify e :=
     [string] identifiers and using them for pretty-printing...  It
     might also be possible to verify this layer, too, by adding a
     partial interpretation function... *)
-Section syn.
-  Context {var : base_type -> Type}.
-  Inductive syntax :=
-  | RegPInv
-  | RegMod
-  | RegMuLow
-  | RegZero
-  | cConstZ : Z -> syntax
-  | cConstBool : bool -> syntax
-  | cLowerHalf : syntax -> syntax
-  | cUpperHalf : syntax -> syntax
-  | cLeftShifted : syntax -> Z -> syntax
-  | cRightShifted : syntax -> Z -> syntax
-  | cVar : var TW -> syntax
-  | cVarC : var Tbool -> syntax
-  | cBind : syntax -> (var TW -> syntax) -> syntax
-  | cBindCarry : syntax -> (var Tbool -> var TW -> syntax) -> syntax
-  | cMul128 : syntax -> syntax -> syntax
-  | cRshi : syntax -> syntax -> Z -> syntax
-  | cSelc : var Tbool -> syntax -> syntax -> syntax
-  | cAddc : var Tbool -> syntax -> syntax -> syntax
-  | cAddm : syntax -> syntax -> syntax
-  | cAdd : syntax -> syntax -> syntax
-  | cSub : syntax -> syntax -> syntax
-  | cPair : syntax -> syntax -> syntax
-  | cAbs {t} : (var t -> syntax) -> syntax
-  | cINVALID {T} (_ : T).
-End syn.
 
-Notation "'Return' x" := (cVar x) (at level 200).
-Notation "'c.Mul128' ( x , A , B ) , b" :=
-  (cBind (cMul128 A B) (fun x => b))
-    (at level 200, b at level 200, format "'c.Mul128' ( x ,  A ,  B ) , '//' b").
+Local Set Decidable Equality Schemes.
+Local Set Boolean Equality Schemes.
+
+Inductive Register :=
+| RegPInv | RegMod | RegMuLow | RegZero
+| y | t1 | t2 | lo | hi | out | src1 | src2 | tmp | q | qHigh | x | xHigh
+| SpecialCarryBit
+| scratch | scratchplus (n : nat).
+
+Notation "'scratch+' n" := (scratchplus n) (format "'scratch+' n", at level 10).
+
+Definition pos_of_Register (r : Register) :=
+  match r with
+  | RegPInv => 1
+  | RegMod => 2
+  | RegMuLow => 3
+  | RegZero => 4
+  | y => 5
+  | t1 => 6
+  | t2 => 7
+  | lo => 8
+  | hi => 9
+  | out => 10
+  | src1 => 11
+  | src2 => 12
+  | tmp => 13
+  | q => 14
+  | qHigh => 15
+  | x => 16
+  | xHigh => 17
+  | SpecialCarryBit => 18
+  | scratch => 19
+  | scratchplus n => 19 + Pos.of_nat (S n)
+  end%positive.
+
+Lemma pos_of_Register_inj x y : pos_of_Register x = pos_of_Register y -> x = y.
+Proof.
+  unfold pos_of_Register; repeat break_match; subst;
+    try rewrite Pos.add_cancel_l; try rewrite Nat2Pos.inj_iff;
+      try solve [ simpl; congruence | intros; exfalso; lia ].
+Qed.
+
+Global Instance RegisterContext {var : base_type -> Type} : Context Register var
+  := ContextOn pos_of_Register (RegisterAssign.pos_context var).
+
+Definition syntax {ops : fancy_machine.instructions (2 * 128)}
+  := Named.expr base_type (interp_base_type ops) op Register.
+
+Class wf_empty {ops} {var} {t} (e : Named.expr base_type (interp_base_type ops) op Register t)
+  := mk_wf_empty : @Named.wf base_type (interp_base_type ops) op Register var _ empty t e.
+Global Hint Extern 0 (wf_empty _) => vm_compute; intros; constructor : typeclass_instances.
+
+(** Assemble a well-typed easily interpretable expression into a
+    syntax tree we can use for pretty-printing. *)
+Section assemble.
+  Context {ops : fancy_machine.instructions (2 * 128)}.
+
+  Definition AssembleSyntax' {t} (e : Expr base_type (interp_base_type _) op t) (ls : list Register)
+    : option (syntax t)
+    := CompileAndEliminateDeadCode e ls.
+  Definition AssembleSyntax {t} e ls (res := @AssembleSyntax' t e ls)
+    := match res return match res with None => _ | _ => _ end with
+       | Some v => v
+       | None => I
+       end.
+
+  Definition dummy_registers (n : nat) : list Register
+    := List.map scratchplus (seq 0 n).
+  Definition DefaultRegisters {t} (e : Expr base_type (interp_base_type _) op t) : list Register
+    := dummy_registers (CountBinders e).
+
+  Definition DefaultAssembleSyntax {t} e := @AssembleSyntax t e (DefaultRegisters e).
+
+  Definition Interp {t} e {wf : wf_empty e}
+    := @Named.interp base_type (interp_base_type _) op Register _ (interp_op _) empty t e wf.
+End assemble.
+
+Export Reflection.Named.Syntax.
+Open Scope nexpr_scope.
+Open Scope ctype_scope.
+Open Scope type_scope.
+Open Scope core_scope.
+
+Notation Return x := (Var x).
+Notation ldi z := (Op OPldi (Const z%Z)).
+Notation "'slet' x := A 'in' b" := (LetIn _ x (Op OPldi (Var A%nexpr)) b%nexpr) : nexpr_scope.
+Notation "'c.Rshi' ( x , A , B , C ) , b" :=
+  (LetIn _ x (Op OPshrd (Pair (Pair (Var A) (Var B)) (Const C%Z))) b)
+    (at level 200, b at level 200, format "'c.Rshi' ( x ,  A ,  B ,  C ) , '//' b").
+Notation "'c.Mul128' ( x , 'c.UpperHalf' ( A ) , 'c.UpperHalf' ( B ) ) , b" :=
+  (LetIn _ x (Op OPmulhwhh (Pair (Var A) (Var B))) b)
+    (at level 200, b at level 200, format "'c.Mul128' ( x ,  'c.UpperHalf' ( A ) ,  'c.UpperHalf' ( B ) ) , '//' b").
+Notation "'c.Mul128' ( x , 'c.UpperHalf' ( A ) , 'c.LowerHalf' ( B ) ) , b" :=
+  (LetIn _ x (Op OPmulhwhl (Pair (Var A) (Var B))) b)
+    (at level 200, b at level 200, format "'c.Mul128' ( x ,  'c.UpperHalf' ( A ) ,  'c.LowerHalf' ( B ) ) , '//' b").
+Notation "'c.Mul128' ( x , 'c.LowerHalf' ( A ) , 'c.LowerHalf' ( B ) ) , b" :=
+  (LetIn _ x (Op OPmulhwll (Pair (Var A) (Var B))) b)
+    (at level 200, b at level 200, format "'c.Mul128' ( x ,  'c.LowerHalf' ( A ) ,  'c.LowerHalf' ( B ) ) , '//' b").
+Notation "'c.LeftShifted' { x , v }" :=
+  (Op OPshl (Pair (Var x) (Const v%Z)))
+    (at level 200, format "'c.LeftShifted' { x ,  v }").
+Notation "'c.RightShifted' { x , v }" :=
+  (Op OPshr (Pair (Var x) (Const v%Z)))
+    (at level 200, format "'c.RightShifted' { x ,  v }").
+
+Notation "'c.Add' ( x , A , B ) , b" :=
+  (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair A B) (Const false))) b)
+    (at level 200, b at level 200, format "'c.Add' ( x ,  A ,  B ) , '//' b").
 Notation "'c.Add' ( x , A , B ) , b" :=
-  (cBindCarry (cAdd A B) (fun _ x => b))
+  (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair (Var A) B) (Const false))) b)
     (at level 200, b at level 200, format "'c.Add' ( x ,  A ,  B ) , '//' b").
 Notation "'c.Add' ( x , A , B ) , b" :=
-  (cBindCarry (cAdd (cVar A) B) (fun _ x => b))
+  (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair A (Var B)) (Const false))) b)
     (at level 200, b at level 200, format "'c.Add' ( x ,  A ,  B ) , '//' b").
-Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , b" :=
-  (cBindCarry (cAdd A B) (fun c x => cBindCarry (cAddc c A1 B1) (fun _ x1 => b)))
-    (at level 200, b at level 200, format "'c.Add' ( x ,  A ,  B ) , '//' 'c.Addc' ( x1 ,  A1 ,  B1 ) , '//' b").
-Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , b" :=
-  (cBindCarry (cAdd A B) (fun c x => cBindCarry (cAddc c (cVar A1) B1) (fun _ x1 => b)))
-    (at level 200, b at level 200, format "'c.Add' ( x ,  A ,  B ) , '//' 'c.Addc' ( x1 ,  A1 ,  B1 ) , '//' b").
-Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , b" :=
-  (cBindCarry (cAdd (cVar A) B) (fun c x => cBindCarry (cAddc c A1 B1) (fun _ x1 => b)))
-    (at level 200, b at level 200, format "'c.Add' ( x ,  A ,  B ) , '//' 'c.Addc' ( x1 ,  A1 ,  B1 ) , '//' b").
-Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , b" :=
-  (cBindCarry (cAdd (cVar A) B) (fun c x => cBindCarry (cAddc c (cVar A1) B1) (fun _ x1 => b)))
-    (at level 200, b at level 200, format "'c.Add' ( x ,  A ,  B ) , '//' 'c.Addc' ( x1 ,  A1 ,  B1 ) , '//' b").
-Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , 'c.Selc' ( x2 , A2 , B2 ) , b" :=
-  (cBindCarry (cAdd A B) (fun c x => cBindCarry (cAddc c A1 B1) (fun c1 x1 => cBind (cSelc c1 A2 B2) (fun x2 => b))))
-    (at level 200, b at level 200, format "'c.Add' ( x ,  A ,  B ) , '//' 'c.Addc' ( x1 ,  A1 ,  B1 ) , '//' 'c.Selc' ( x2 ,  A2 ,  B2 ) , '//' b").
-Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , 'c.Selc' ( x2 , A2 , B2 ) , b" :=
-  (cBindCarry (cAdd (cVar A) B) (fun c x => cBindCarry (cAddc c A1 B1) (fun c1 x1 => cBind (cSelc c1 A2 B2) (fun x2 => b))))
-    (at level 200, b at level 200, format "'c.Add' ( x ,  A ,  B ) , '//' 'c.Addc' ( x1 ,  A1 ,  B1 ) , '//' 'c.Selc' ( x2 ,  A2 ,  B2 ) , '//' b").
-Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , 'c.Selc' ( x2 , A2 , B2 ) , b" :=
-  (cBindCarry (cAdd A B) (fun c x => cBindCarry (cAddc c (cVar A1) B1) (fun c1 x1 => cBind (cSelc c1 A2 B2) (fun x2 => b))))
-    (at level 200, b at level 200, format "'c.Add' ( x ,  A ,  B ) , '//' 'c.Addc' ( x1 ,  A1 ,  B1 ) , '//' 'c.Selc' ( x2 ,  A2 ,  B2 ) , '//' b").
-Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , 'c.Selc' ( x2 , A2 , B2 ) , b" :=
-  (cBindCarry (cAdd (cVar A) B) (fun c x => cBindCarry (cAddc c (cVar A1) B1) (fun c1 x1 => cBind (cSelc c1 A2 B2) (fun x2 => b))))
-    (at level 200, b at level 200, format "'c.Add' ( x ,  A ,  B ) , '//' 'c.Addc' ( x1 ,  A1 ,  B1 ) , '//' 'c.Selc' ( x2 ,  A2 ,  B2 ) , '//' b").
-Notation "'c.Add' ( x , A , B ) , 'c.Addc' ( x1 , A1 , B1 ) , 'c.Selc' ( x2 , A2 , B2 ) , b" :=
-  (cBindCarry (cAdd (cVar A) (cVar B)) (fun c x => cBindCarry (cAddc c (cVar A1) (cVar B1)) (fun c1 x1 => cBind (cSelc c1 A2 B2) (fun x2 => b))))
-    (at level 200, b at level 200, format "'c.Add' ( x ,  A ,  B ) , '//' 'c.Addc' ( x1 ,  A1 ,  B1 ) , '//' 'c.Selc' ( x2 ,  A2 ,  B2 ) , '//' b").
+Notation "'c.Add' ( x , A , B ) , b" :=
+  (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair (Var A) (Var B)) (Const false))) b)
+    (at level 200, b at level 200, format "'c.Add' ( x ,  A ,  B ) , '//' b").
+Notation "'c.Addc' ( x , A , B ) , b" :=
+  (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair A B) (Var SpecialCarryBit))) b)
+    (at level 200, b at level 200, format "'c.Addc' ( x ,  A ,  B ) , '//' b").
+Notation "'c.Addc' ( x , A , B ) , b" :=
+  (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair (Var A) B) (Var SpecialCarryBit))) b)
+    (at level 200, b at level 200, format "'c.Addc' ( x ,  A ,  B ) , '//' b").
+Notation "'c.Addc' ( x , A , B ) , b" :=
+  (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair A (Var B)) (Var SpecialCarryBit))) b)
+    (at level 200, b at level 200, format "'c.Addc' ( x ,  A ,  B ) , '//' b").
+Notation "'c.Addc' ( x , A , B ) , b" :=
+  (LetIn _ (pair SpecialCarryBit x) (Op OPadc (Pair (Pair (Var A) (Var B)) (Var SpecialCarryBit))) b)
+    (at level 200, b at level 200, format "'c.Addc' ( x ,  A ,  B ) , '//' b").
 
 Notation "'c.Sub' ( x , A , B ) , b" :=
-  (cBindCarry (cSub A B) (fun _ x => b))
+  (LetIn _ (pair SpecialCarryBit x) (Op OPsubc (Pair (Pair A B) (Const false))) b)
     (at level 200, b at level 200, format "'c.Sub' ( x ,  A ,  B ) , '//' b").
 Notation "'c.Sub' ( x , A , B ) , b" :=
-  (cBindCarry (cSub (cVar A) B) (fun _ x => b))
+  (LetIn _ (pair SpecialCarryBit x) (Op OPsubc (Pair (Pair (Var A) B) (Const false))) b)
     (at level 200, b at level 200, format "'c.Sub' ( x ,  A ,  B ) , '//' b").
 Notation "'c.Sub' ( x , A , B ) , b" :=
-  (cBindCarry (cSub A (cVar B)) (fun _ x => b))
+  (LetIn _ (pair SpecialCarryBit x) (Op OPsubc (Pair (Pair A (Var B)) (Const false))) b)
     (at level 200, b at level 200, format "'c.Sub' ( x ,  A ,  B ) , '//' b").
 Notation "'c.Sub' ( x , A , B ) , b" :=
-  (cBindCarry (cSub (cVar A) (cVar B)) (fun _ x => b))
+  (LetIn _ (pair SpecialCarryBit x) (Op OPsubc (Pair (Pair (Var A) (Var B)) (Const false))) b)
     (at level 200, b at level 200, format "'c.Sub' ( x ,  A ,  B ) , '//' b").
 
 Notation "'c.Addm' ( x , A , B ) , b" :=
-  (cBind (cAddm A B) (fun x => b))
+  (LetIn _ x (Op OPaddm (Pair (Pair A B) (Var RegMod))) b)
     (at level 200, b at level 200, format "'c.Addm' ( x ,  A ,  B ) , '//' b").
 Notation "'c.Addm' ( x , A , B ) , b" :=
-  (cBind (cAddm A (cVar B)) (fun x => b))
+  (LetIn _ x (Op OPaddm (Pair (Pair (Var A) B) (Var RegMod))) b)
     (at level 200, b at level 200, format "'c.Addm' ( x ,  A ,  B ) , '//' b").
 Notation "'c.Addm' ( x , A , B ) , b" :=
-  (cBind (cAddm (cVar A) B) (fun x => b))
+  (LetIn _ x (Op OPaddm (Pair (Pair A (Var B)) (Var RegMod))) b)
     (at level 200, b at level 200, format "'c.Addm' ( x ,  A ,  B ) , '//' b").
 Notation "'c.Addm' ( x , A , B ) , b" :=
-  (cBind (cAddm (cVar A) (cVar B)) (fun x => b))
+  (LetIn _ x (Op OPaddm (Pair (Pair (Var A) (Var B)) (Var RegMod))) b)
     (at level 200, b at level 200, format "'c.Addm' ( x ,  A ,  B ) , '//' b").
 
-Notation "'c.Rshi' ( x , A , B , C ) , b" :=
-  (cBind (cRshi (cVar A) (cVar B) C) (fun x => b))
-    (at level 200, b at level 200, format "'c.Rshi' ( x ,  A ,  B ,  C ) , '//' b").
-
-Notation "'c.LowerHalf' ( x )" :=
-  (cLowerHalf x)
-    (at level 200, format "'c.LowerHalf' ( x )").
-Notation "'c.LowerHalf' ( x )" :=
-  (cLowerHalf (cVar x))
-    (at level 200, format "'c.LowerHalf' ( x )").
-Notation "'c.UpperHalf' ( x )" :=
-  (cUpperHalf x)
-    (at level 200, format "'c.UpperHalf' ( x )").
-Notation "'c.UpperHalf' ( x )" :=
-  (cUpperHalf (cVar x))
-    (at level 200, format "'c.UpperHalf' ( x )").
-Notation "'c.LeftShifted' { x , v }" :=
-  (cLeftShifted x v)
-    (at level 200, format "'c.LeftShifted' { x ,  v }").
-Notation "'c.LeftShifted' { x , v }" :=
-  (cLeftShifted (cVar x) v)
-    (at level 200, format "'c.LeftShifted' { x ,  v }").
-Notation "'c.RightShifted' { x , v }" :=
-  (cRightShifted x v)
-    (at level 200, format "'c.RightShifted' { x ,  v }").
-Notation "'c.RightShifted' { x , v }" :=
-  (cRightShifted (cVar x) v)
-    (at level 200, format "'c.RightShifted' { x ,  v }").
-Notation "'λ'  x .. y , t" := (cAbs (fun x => .. (cAbs (fun y => t)) ..))
-  (at level 200, x binder, y binder, right associativity).
-
-Definition Syntax := forall var, @syntax var.
-
-(** Assemble a well-typed easily interpretable expression into a
-    syntax tree we can use for pretty-printing. *)
-Section assemble.
-  Context (ops : fancy_machine.instructions (2 * 128)).
-
-  Section with_var.
-    Context {var : base_type -> Type}.
-
-    Fixpoint assemble_syntax_const
-             {t}
-      : interp_flat_type_gen (interp_base_type _) t -> @syntax var
-      := match t return interp_flat_type_gen (interp_base_type _) t -> @syntax var with
-         | Tbase TZ => cConstZ
-         | Tbase Tbool => cConstBool
-         | Tbase t => fun _ => cINVALID t
-         | Prod A B => fun xy => cPair (@assemble_syntax_const A (fst xy))
-                                       (@assemble_syntax_const B (snd xy))
-         end.
-
-    Definition assemble_syntaxf_step
-               (assemble_syntaxf : forall {t} (v : @Syntax.exprf base_type (interp_base_type _) op (fun _ => @syntax var) t), @syntax var)
-               {t} (v : @Syntax.exprf base_type (interp_base_type _) op (fun _ => @syntax var) t) : @syntax var.
-    Proof.
-      refine match v return @syntax var with
-             | Syntax.Const t x => assemble_syntax_const x
-             | Syntax.Var _ x => x
-             | Syntax.Op t1 tR op args
-               => let v := @assemble_syntaxf t1 args in
-                 (* handle both associativities of pairs in 3-ary
-                    operators, in case we ever change the
-                    associativity *)
-                  match op, v with
-                  | OPldi    , cConstZ 0 => RegZero
-                  | OPldi    , cConstZ v => cINVALID v
-                  | OPldi    , RegZero => RegZero
-                  | OPldi    , RegMod => RegMod
-                  | OPldi    , RegMuLow => RegMuLow
-                  | OPldi    , RegPInv => RegPInv
-                  | OPshrd   , cPair x (cPair y (cConstZ n)) => cRshi x y n
-                  | OPshrd   , cPair (cPair x y) (cConstZ n) => cRshi x y n
-                  | OPshl    , cPair w (cConstZ n) => cLeftShifted w n
-                  | OPshr    , cPair w (cConstZ n) => cRightShifted w n
-                  | OPmkl    , _ => cINVALID op
-                  | OPadc    , cPair (cPair x y) (cVarC c) => cAddc c x y
-                  | OPadc    , cPair x (cPair y (cVarC c)) => cAddc c x y
-                  | OPadc    , cPair (cPair x y) (cConstBool false) => cAdd x y
-                  | OPadc    , cPair x (cPair y (cConstBool false)) => cAdd x y
-                  | OPsubc   , cPair (cPair x y) (cConstBool false) => cSub x y
-                  | OPsubc   , cPair x (cPair y (cConstBool false)) => cSub x y
-                  | OPmulhwll, cPair x y => cMul128 (cLowerHalf x) (cLowerHalf y)
-                  | OPmulhwhl, cPair x y => cMul128 (cUpperHalf x) (cLowerHalf y)
-                  | OPmulhwhh, cPair x y => cMul128 (cUpperHalf x) (cUpperHalf y)
-                  | OPselc   , cPair (cVarC c) (cPair x y) => cSelc c x y
-                  | OPselc   , cPair (cPair (cVarC c) x) y => cSelc c x y
-                  | OPaddm   , cPair x (cPair y RegMod) => cAddm x y
-                  | OPaddm   , cPair (cPair x y) RegMod => cAddm x y
-                  | _, _ => cINVALID op
-                  end
-             | Syntax.LetIn tx ex _ eC
-               => let ex' := @assemble_syntaxf _ ex in
-                 let eC' := fun x => @assemble_syntaxf _ (eC x) in
-                 let special := match ex' with
-                                | RegZero as ex'' | RegMuLow as ex'' | RegMod as ex'' | RegPInv as ex''
-                                | cUpperHalf _ as ex'' | cLowerHalf _ as ex''
-                                | cLeftShifted _ _ as ex''
-                                | cRightShifted _ _ as ex''
-                                  => Some ex''
-                                | _ => None
-                                end in
-                 match special, tx return (interp_flat_type_gen _ tx -> _) -> _ with
-                 | Some x, Tbase _ => fun eC' => eC' x
-                 | _, Tbase TW
-                   => fun eC' => cBind ex' (fun x => eC' (cVar x))
-                 | _, Prod (Tbase Tbool) (Tbase TW)
-                   => fun eC' => cBindCarry ex' (fun c x => eC' (cVarC c, cVar x))
-                 | _, _
-                   => fun _ => cINVALID (fun x : Prop => x)
-                 end eC'
-             | Syntax.Pair _ ex _ ey
-               => cPair (@assemble_syntaxf _ ex) (@assemble_syntaxf _ ey)
-             end.
-    Defined.
-
-    Fixpoint assemble_syntaxf {t} v {struct v} : @syntax var
-      := @assemble_syntaxf_step (@assemble_syntaxf) t v.
-    Fixpoint assemble_syntax {t} (v : @Syntax.expr base_type (interp_base_type _) op (fun _ => @syntax var) t) (args : list (@syntax var)) {struct v}
-      : @syntax var
-      := match v, args return @syntax var with
-         | Syntax.Return _ x, _ => assemble_syntaxf x
-         | Syntax.Abs _ _ f, nil => cAbs (fun x => @assemble_syntax _ (f (cVar x)) args)
-         | Syntax.Abs _ _ f, cons v vs => @assemble_syntax _ (f v) vs
-         end.
-  End with_var.
-
-  Definition AssembleSyntax {t} (v : Syntax.Expr _ _ _ t) (args : list Syntax) : Syntax
-    := fun var => @assemble_syntax var t (v _) (List.map (fun f => f var) args).
-End assemble.
+Notation "'c.Selc' ( x , A , B ) , b" :=
+  (LetIn _ x (Op OPselc (Pair (Pair (Var SpecialCarryBit) A) B)) b)
+    (at level 200, b at level 200, format "'c.Selc' ( x ,  A ,  B ) , '//' b").
+Notation "'c.Selc' ( x , A , B ) , b" :=
+  (LetIn _ x (Op OPselc (Pair (Pair (Var SpecialCarryBit) (Var A)) B)) b)
+    (at level 200, b at level 200, format "'c.Selc' ( x ,  A ,  B ) , '//' b").
+Notation "'c.Selc' ( x , A , B ) , b" :=
+  (LetIn _ x (Op OPselc (Pair (Pair (Var SpecialCarryBit) A) (Var B))) b)
+    (at level 200, b at level 200, format "'c.Selc' ( x ,  A ,  B ) , '//' b").
+Notation "'c.Selc' ( x , A , B ) , b" :=
+  (LetIn _ x (Op OPselc (Pair (Pair (Var SpecialCarryBit) (Var A)) (Var B))) b)
+    (at level 200, b at level 200, format "'c.Selc' ( x ,  A ,  B ) , '//' b").