move src/Experiments/NewPipeline/ to src/

1 files changed, 1806 insertions, 0 deletions

diff --git a/src/Language.v b/src/Language.v
new file mode 100644
index 000000000..eba5cf85a
--- /dev/null
+++ b/src/Language.v
@@ -0,0 +1,1806 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.FSets.FMapPositive.
+Require Import Coq.Bool.Bool.
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Relations.Relation_Definitions.
+Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn.
+Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Prod.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.ZRange.Operations.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.Notations.
+Require Import Crypto.Util.CPSNotations.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.Tactics.RunTacticAsConstr.
+Require Import Crypto.Util.Tactics.DebugPrint.
+Import ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope.
+
+Module Compilers.
+  Local Set Boolean Equality Schemes.
+  Local Set Decidable Equality Schemes.
+  Module Reify.
+    (** Change this with [Ltac reify_debug_level ::= constr:(1).] to get
+        more debugging. *)
+    Ltac debug_level := constr:(0%nat).
+
+    Tactic Notation "debug_enter_reify_idtac" ident(funname) uconstr(e)
+      := idtac funname ": Attempting to reify:" e.
+    Tactic Notation "debug_leave_reify_success_idtac" ident(funname) uconstr(e) uconstr(ret)
+      := idtac funname ": Success in reifying:" e "as" ret.
+    Tactic Notation "debug_leave_reify_failure_idtac" ident(funname) uconstr(e)
+      := idtac funname ": Failure in reifying:" e.
+    Ltac check_debug_level_then_Set _ :=
+      let lvl := debug_level in
+      lazymatch type of lvl with
+      | nat => constr:(Set)
+      | ?T => constr_run_tac ltac:(fun _ => idtac "Error: debug_level should have type nat but instead has type" T)
+      end.
+    Ltac debug0 tac :=
+      constr_run_tac tac.
+    Ltac debug1 tac :=
+      let lvl := debug_level in
+      lazymatch lvl with
+      | S _ => constr_run_tac tac
+      | _ => check_debug_level_then_Set ()
+      end.
+    Ltac debug2 tac :=
+      let lvl := debug_level in
+      lazymatch lvl with
+      | S (S _) => constr_run_tac tac
+      | _ => check_debug_level_then_Set ()
+      end.
+    Ltac debug3 tac :=
+      let lvl := debug_level in
+      lazymatch lvl with
+      | S (S (S _)) => constr_run_tac tac
+      | _ => check_debug_level_then_Set ()
+      end.
+    Ltac debug_enter_reify_base_type e := debug2 ltac:(fun _ => debug_enter_reify_idtac reify_base_type e).
+    Ltac debug_enter_reify_type e := debug2 ltac:(fun _ => debug_enter_reify_idtac reify_type e).
+    Ltac debug_enter_reify_in_context e := debug2 ltac:(fun _ => debug_enter_reify_idtac reify_in_context e).
+    Ltac debug_leave_reify_in_context_success e ret := debug3 ltac:(fun _ => debug_leave_reify_success_idtac reify_in_context e ret).
+    Ltac debug_leave_reify_in_context_failure e
+      := let dummy := debug0 ltac:(fun _ => debug_leave_reify_failure_idtac reify_in_context e) in
+         constr:(I : I).
+    Ltac debug_leave_reify_base_type_failure e
+      := let dummy := debug0 ltac:(fun _ => debug_leave_reify_failure_idtac reify_base_type e) in
+         constr:(I : I).
+    Tactic Notation "idtac_reify_in_context_case" ident(case) :=
+      idtac "reify_in_context:" case.
+    Ltac debug_reify_in_context_case tac :=
+      debug3 tac.
+    Ltac debug_enter_reify_abs e := debug2 ltac:(fun _ => debug_enter_reify_idtac reify_abs e).
+  End Reify.
+
+  Module type.
+    Inductive type {base_type : Type} := base (t : base_type) | arrow (s d : type).
+    Global Arguments type : clear implicits.
+
+    Fixpoint final_codomain {base_type} (t : type base_type) : base_type
+      := match t with
+         | base t
+           => t
+         | arrow s d => @final_codomain base_type d
+         end.
+
+    Fixpoint uncurried_domain {base_type} prod s (t : type base_type) : type base_type
+      := match t with
+         | base t
+           => s
+         | arrow s' d => @uncurried_domain base_type prod (prod s s') d
+         end.
+
+    Fixpoint for_each_lhs_of_arrow {base_type} (f : type base_type -> Type) (t : type base_type) : Type
+      := match t with
+         | base t => unit
+         | arrow s d => f s * @for_each_lhs_of_arrow _ f d
+         end.
+
+    Fixpoint andb_each_lhs_of_arrow {base_type} (f : type base_type -> bool) (t : type base_type) : bool
+      := match t with
+         | base t => true
+         | arrow s d => andb (f s) (@andb_each_lhs_of_arrow _ f d)
+         end.
+
+    (** Denote [type]s into their interpretation in [Type]/[Set] *)
+    Fixpoint interp {base_type} (base_interp : base_type -> Type) (t : type base_type) : Type
+      := match t with
+         | base t => base_interp t
+         | arrow s d => @interp _ base_interp s -> @interp _ base_interp d
+         end.
+
+    Fixpoint related {base_type} {base_interp : base_type -> Type} (R : forall t, relation (base_interp t)) {t : type base_type}
+      : relation (interp base_interp t)
+      := match t with
+         | base t => R t
+         | arrow s d => @related _ _ R s ==> @related _ _ R d
+         end%signature.
+
+    Notation eqv := (@related _ _ (fun _ => eq)).
+
+    Fixpoint related_hetero {base_type} {base_interp1 base_interp2 : base_type -> Type}
+             (R : forall t, base_interp1 t -> base_interp2 t -> Prop) {t : type base_type}
+      : interp base_interp1 t -> interp base_interp2 t -> Prop
+      := match t with
+         | base t => R t
+         | arrow s d => respectful_hetero _ _ _ _ (@related_hetero _ _ _ R s) (fun _ _ => @related_hetero _ _ _ R d)
+         end%signature.
+
+    Fixpoint related_hetero3 {base_type} {base_interp1 base_interp2 base_interp3 : base_type -> Type}
+             (R : forall t, base_interp1 t -> base_interp2 t -> base_interp3 t -> Prop) {t : type base_type}
+      : interp base_interp1 t -> interp base_interp2 t -> interp base_interp3 t -> Prop
+      := match t with
+         | base t => R t
+         | arrow s d
+           => fun f g h
+              => forall x y z, @related_hetero3 _ _ _ _ R s x y z -> @related_hetero3 _ _ _ _ R d (f x) (g y) (h z)
+         end.
+
+    Fixpoint app_curried {base_type} {f : base_type -> Type} {t : type base_type}
+      : interp f t -> for_each_lhs_of_arrow (interp f) t -> f (final_codomain t)
+      := match t with
+         | base t => fun v _ => v
+         | arrow s d => fun F x_xs => @app_curried _ f d (F (fst x_xs)) (snd x_xs)
+         end.
+
+    Fixpoint app_curried_gen {base_type} {f : type base_type -> Type} (app : forall s d, f (arrow s d) -> f s -> f d)
+             {t : type base_type}
+      : f t -> for_each_lhs_of_arrow f t -> f (base (final_codomain t))
+      := match t with
+         | base t => fun v _ => v
+         | arrow s d => fun F x_xs => @app_curried_gen _ f app d (app _ _ F (fst x_xs)) (snd x_xs)
+         end.
+
+    Fixpoint map_for_each_lhs_of_arrow {base_type} {f g : type base_type -> Type}
+             (F : forall t, f t -> g t)
+             {t}
+      : for_each_lhs_of_arrow f t -> for_each_lhs_of_arrow g t
+      := match t with
+         | base t => fun 'tt => tt
+         | arrow s d => fun '(x, xs) => (F s x, @map_for_each_lhs_of_arrow _ f g F d xs)
+         end.
+
+    Fixpoint andb_bool_for_each_lhs_of_arrow {base_type} {f g : type base_type -> Type}
+             (R : forall t, f t -> g t -> bool)
+             {t}
+      : for_each_lhs_of_arrow f t -> for_each_lhs_of_arrow g t -> bool
+      := match t with
+         | base t => fun _ _ => true
+         | arrow s d => fun x_xs y_ys => R s (fst x_xs) (fst y_ys) && @andb_bool_for_each_lhs_of_arrow _ f g R d (snd x_xs) (snd y_ys)
+         end%bool.
+
+    Fixpoint and_for_each_lhs_of_arrow {base_type} {f g : type base_type -> Type}
+             (R : forall t, f t -> g t -> Prop)
+             {t}
+      : for_each_lhs_of_arrow f t -> for_each_lhs_of_arrow g t -> Prop
+      := match t with
+         | base t => fun _ _ => True
+         | arrow s d => fun x_xs y_ys => R s (fst x_xs) (fst y_ys) /\ @and_for_each_lhs_of_arrow _ f g R d (snd x_xs) (snd y_ys)
+         end.
+
+    Definition is_base {base_type} (t : type base_type) : bool
+      := match t with
+         | type.base _ => true
+         | type.arrow _ _ => false
+         end.
+
+    Definition is_not_higher_order {base_type} : type base_type -> bool
+      := andb_each_lhs_of_arrow is_base.
+
+    Section interpM.
+      Context {base_type} (M : Type -> Type) (base_interp : base_type -> Type).
+      (** half-monadic denotation function; denote [type]s into their
+          interpretation in [Type]/[Set], wrapping the codomain of any
+          arrow in [M]. *)
+      Fixpoint interpM (t : type base_type) : Type
+        := match t with
+           | base t => base_interp t
+           | arrow s d => @interpM s -> M (@interpM d)
+           end.
+      Fixpoint interpM_final' (withM : bool) (t : type base_type)
+        := match t with
+           | base t => if withM then M (base_interp t) else base_interp t
+           | arrow s d => interpM_final' false s -> interpM_final' true d
+           end.
+      Definition interpM_final := interpM_final' true.
+
+      Fixpoint interpM_return (t : type base_type) : M (base_interp (final_codomain t)) -> interpM_final t
+        := match t with
+           | base t => fun v => v
+           | arrow s d => fun v _ => @interpM_return d v
+           end.
+    End interpM.
+
+    Definition domain {base_type} (default : base_type) (t : type base_type)
+      : type base_type
+      := match t with
+         | arrow s d => s
+         | base _ => base default
+         end.
+
+    Definition codomain {base_type} (t : type base_type) : type base_type
+      := match t with
+         | arrow s d => d
+         | t => t
+         end.
+
+    Section transport_cps.
+      Context {base_type}
+              (try_make_transport_base_type_cps : forall (P : base_type -> Type) t1 t2, ~> option (P t1 -> P t2)).
+
+      Fixpoint try_make_transport_cps (P : type base_type -> Type) (t1 t2 : type base_type)
+        : ~> option (P t1 -> P t2)
+        := match t1, t2 with
+           | base t1, base t2 => try_make_transport_base_type_cps (fun t => P (base t)) t1 t2
+           | arrow s1 d1, arrow s2 d2
+             => (trs <-- try_make_transport_cps (fun s => P (arrow s _)) _ _;
+                  trd <-- try_make_transport_cps (fun d => P (arrow _ d)) _ _;
+                return (Some (fun v => trd (trs v))))
+           | base _, _
+           | arrow _ _, _
+             => (return None)
+           end%cps.
+
+      Definition try_transport_cps (P : type base_type -> Type) (t1 t2 : type base_type) (v : P t1) : ~> option (P t2)
+        := (tr <-- try_make_transport_cps P t1 t2;
+            return (Some (tr v)))%cps.
+
+      Definition try_transport (P : type base_type -> Type) (t1 t2 : type base_type) (v : P t1) : option (P t2)
+        := try_transport_cps P t1 t2 v _ id.
+    End transport_cps.
+
+    (*
+    Fixpoint try_transport {base_type}
+             (try_transport_base_type : forall (P : base_type -> Type) t1 t2, P t1 -> option (P t2))
+             (P : type base_type -> Type) (t1 t2 : type base_type) : P t1 -> option (P t2)
+      := match t1, t2 return P t1 -> option (P t2) with
+         | base t1, base t2
+           => try_transport_base_type (fun t => P (base t)) t1 t2
+         | arrow s d, arrow s' d'
+           => fun v
+             => (v <- (try_transport
+                       try_transport_base_type (fun s => P (arrow s d))
+                       s s' v);
+                  (try_transport
+                     try_transport_base_type (fun d => P (arrow s' d))
+                     d d' v))%option
+         | base _, _
+         | arrow _ _, _
+           => fun _ => None
+         end.
+*)
+
+    Ltac reify base_reify base_type ty :=
+      let __ := Reify.debug_enter_reify_type ty in
+      let reify_rec t := reify base_reify base_type t in
+      lazymatch eval cbv beta in ty with
+      | ?A -> ?B
+        => let rA := reify_rec A in
+           let rB := reify_rec B in
+           constr:(@arrow base_type rA rB)
+      | @interp _ _ ?T => T
+      | _ => let rt := base_reify ty in
+             constr:(@base base_type rt)
+      end.
+  End type.
+  Notation type := type.type.
+  Delimit Scope etype_scope with etype.
+  Bind Scope etype_scope with type.type.
+  Infix "->" := type.arrow : etype_scope.
+  Infix "==" := type.eqv : type_scope.
+  Module base.
+    Local Notation einterp := type.interp.
+    Module type.
+      Inductive base := unit | Z | bool | nat. (* Not Variant because COQBUG(https://github.com/coq/coq/issues/7738) *)
+      Inductive type := type_base (t : base) | prod (A B : type) | list (A : type).
+      Global Coercion type_base : base >-> type.
+    End type.
+    Global Coercion type.type_base : type.base >-> type.type.
+    Notation type := type.type.
+    Definition base_interp (ty : type.base)
+      := match ty with
+         | type.unit => Datatypes.unit
+         | type.Z => BinInt.Z
+         | type.bool => Datatypes.bool
+         | type.nat => Datatypes.nat
+         end.
+    Fixpoint interp (ty : type)
+      := match ty with
+         | type.type_base t => base_interp t
+         | type.prod A B => interp A * interp B
+         | type.list A => Datatypes.list (interp A)
+         end%type.
+
+    Definition try_make_base_transport_cps
+               (P : type.base -> Type) (t1 t2 : type.base)
+      : ~> option (P t1 -> P t2)
+      := match t1, t2 with
+         | type.unit, type.unit
+         | type.Z, type.Z
+         | type.bool, type.bool
+         | type.nat, type.nat
+           => (return (Some id))
+         | type.unit, _
+         | type.Z, _
+         | type.bool, _
+         | type.nat, _
+           => (return None)
+         end%cps.
+    Fixpoint try_make_transport_cps
+             (P : type -> Type) (t1 t2 : type)
+      : ~> option (P t1 -> P t2)
+      := match t1, t2 with
+         | type.type_base t1, type.type_base t2
+           => try_make_base_transport_cps (fun t => P (type.type_base t)) t1 t2
+         | type.prod A B, type.prod A' B'
+           => (trA <-- try_make_transport_cps (fun A => P (type.prod A _)) _ _;
+                trB <-- try_make_transport_cps (fun B => P (type.prod _ B)) _ _;
+              return (Some (fun v => trB (trA v))))
+         | type.list A, type.list A' => try_make_transport_cps (fun A => P (type.list A)) A A'
+         | type.type_base _, _
+         | type.prod _ _, _
+         | type.list _, _
+           => (return None)
+         end%cps.
+
+    Definition try_transport_cps (P : type -> Type) (t1 t2 : type) (v : P t1) : ~> option (P t2)
+      := (tr <-- try_make_transport_cps P t1 t2;
+            return (Some (tr v)))%cps.
+
+    Definition try_transport (P : type -> Type) (t1 t2 : type) (v : P t1) : option (P t2)
+      := try_transport_cps P t1 t2 v _ id.
+    (*
+    Fixpoint try_transport
+             (P : type -> Type) (t1 t2 : type) : P t1 -> option (P t2)
+      := match t1, t2 return P t1 -> option (P t2) with
+         | type.unit, type.unit
+         | type.Z, type.Z
+         | type.bool, type.bool
+         | type.nat, type.nat
+           => @Some _
+         | type.list A, type.list A'
+           => @try_transport (fun A => P (type.list A)) A A'
+         | type.prod s d, type.prod s' d'
+           => fun v
+              => (v <- (try_transport (fun s => P (type.prod s d)) s s' v);
+                    (try_transport (fun d => P (type.prod s' d)) d d' v))%option
+
+         | type.unit, _
+         | type.Z, _
+         | type.bool, _
+         | type.nat, _
+         | type.prod _ _, _
+         | type.list _, _
+           => fun _ => None
+         end.
+     *)
+
+    Ltac reify_base ty :=
+      let __ := Reify.debug_enter_reify_base_type ty in
+      lazymatch eval cbv beta in ty with
+      | Datatypes.unit => type.unit
+      | Datatypes.nat => type.nat
+      | Datatypes.bool => type.bool
+      | BinInt.Z => type.Z
+      | interp (type.type_base ?T) => T
+      | @einterp type interp (@Compilers.type.base type (type.type_base ?T)) => T
+      | _ => let __ := match goal with
+                      | _ => fail 1 "Unrecognized type:" ty
+                      end in
+            constr:(I : I)
+      end.
+    Ltac reify ty :=
+      let __ := Reify.debug_enter_reify_base_type ty in
+      lazymatch eval cbv beta in ty with
+      | Datatypes.prod ?A ?B
+        => let rA := reify A in
+          let rB := reify B in
+          constr:(type.prod rA rB)
+      | Datatypes.list ?T
+        => let rT := reify T in
+          constr:(type.list rT)
+      | interp ?T => T
+      | @einterp type interp (@Compilers.type.base type ?T) => T
+      | ?ty => let rT := reify_base ty in
+              constr:(@type.type_base rT)
+      end.
+    Notation reify_base t := (ltac:(let rt := reify_base t in exact rt)) (only parsing).
+    Notation reify t := (ltac:(let rt := reify t in exact rt)) (only parsing).
+    Notation reify_norm_base t := (ltac:(let t' := eval cbv in t in let rt := reify_base t' in exact rt)) (only parsing).
+    Notation reify_norm t := (ltac:(let t' := eval cbv in t in let rt := reify t' in exact rt)) (only parsing).
+    Notation reify_base_type_of e := (reify_base ((fun t (_ : t) => t) _ e)) (only parsing).
+    Notation reify_type_of e := (reify ((fun t (_ : t) => t) _ e)) (only parsing).
+    Notation reify_norm_base_type_of e := (reify_norm_base ((fun t (_ : t) => t) _ e)) (only parsing).
+    Notation reify_norm_type_of e := (reify_norm ((fun t (_ : t) => t) _ e)) (only parsing).
+  End base.
+  Global Coercion base.type.type_base : base.type.base >-> base.type.type.
+  Bind Scope etype_scope with base.type.
+  Infix "*" := base.type.prod : etype_scope.
+  Notation "()" := (base.type.type_base base.type.unit) : etype_scope.
+
+  Module expr.
+    Section with_var.
+      Context {base_type : Type}.
+      Local Notation type := (type base_type).
+      Context {ident : type -> Type}
+              {var : type -> Type}.
+
+      Inductive expr : type -> Type :=
+      | Ident {t} (idc : ident t) : expr t
+      | Var {t} (v : var t) : expr t
+      | Abs {s d} (f : var s -> expr d) : expr (s -> d)
+      | App {s d} (f : expr (s -> d)) (x : expr s) : expr d
+      | LetIn {A B} (x : expr A) (f : var A -> expr B) : expr B
+      .
+    End with_var.
+
+    Fixpoint interp {base_type ident} {interp_base_type : base_type -> Type}
+             (interp_ident : forall t, ident t -> type.interp interp_base_type t)
+             {t} (e : @expr base_type ident (type.interp interp_base_type) t)
+      : type.interp interp_base_type t
+      := match e in expr t return type.interp _ t with
+         | Ident t idc => interp_ident _ idc
+         | Var t v => v
+         | Abs s d f => fun x : type.interp interp_base_type s
+                        => @interp _ _ _ interp_ident _ (f x)
+         | App s d f x => (@interp _ _ _ interp_ident _ f)
+                            (@interp _ _ _ interp_ident _ x)
+         | LetIn A B x f
+           => dlet y := @interp _ _ _ interp_ident _ x in
+               @interp _ _ _ interp_ident _ (f y)
+         end.
+
+    Section with_interp.
+      Context {base_type : Type}
+              {ident : type base_type -> Type}
+              {interp_base_type : base_type -> Type}
+              (interp_ident : forall t, ident t -> type.interp interp_base_type t).
+
+      Fixpoint interp_related_gen
+               {var : type base_type -> Type}
+               (R : forall t, var t -> type.interp interp_base_type t -> Prop)
+               {t} (e : @expr base_type ident var t)
+        : type.interp interp_base_type t -> Prop
+        := match e in expr t return type.interp interp_base_type t -> Prop with
+           | expr.Var t v1 => R t v1
+           | expr.App s d f x
+             => fun v2
+                => exists fv xv,
+                    @interp_related_gen var R _ f fv
+                    /\ @interp_related_gen var R _ x xv
+                    /\ fv xv = v2
+           | expr.Ident t idc
+             => fun v2 => interp_ident _ idc == v2
+           | expr.Abs s d f1
+             => fun f2
+                => forall x1 x2,
+                    R _ x1 x2
+                    -> @interp_related_gen var R d (f1 x1) (f2 x2)
+           | expr.LetIn s d x f (* combine the App rule with the Abs rule *)
+             => fun v2
+                => exists fv xv,
+                    @interp_related_gen var R _ x xv
+                    /\ (forall x1 x2,
+                           R _ x1 x2
+                           -> @interp_related_gen var R d (f x1) (fv x2))
+                    /\ fv xv = v2
+           end.
+
+      Definition interp_related {t} (e : @expr base_type ident (type.interp interp_base_type) t) : type.interp interp_base_type t -> Prop
+        := @interp_related_gen (type.interp interp_base_type) (@type.eqv) t e.
+    End with_interp.
+
+    Definition Expr {base_type ident} t := forall var, @expr base_type ident var t.
+    Definition APP {base_type ident s d} (f : Expr (s -> d)) (x : Expr s) : Expr d
+      := fun var => @App base_type ident var s d (f var) (x var).
+
+    Definition Interp {base_type ident interp_base_type} interp_ident {t} (e : @Expr base_type ident t)
+      : type.interp interp_base_type t
+      := @interp base_type ident interp_base_type interp_ident t (e _).
+
+    (** [Interp (APP _ _)] is the same thing as Gallina application of
+        the [Interp]retations of the two arguments to [APP]. *)
+    Definition Interp_APP {base_type ident interp_base_type interp_ident} {s d} (f : @Expr base_type ident (s -> d)) (x : @Expr base_type ident s)
+      : @Interp base_type ident interp_base_type interp_ident _ (APP f x)
+        = Interp interp_ident f (Interp interp_ident x)
+      := eq_refl.
+
+    (** Same as [Interp_APP], but for any reflexive relation, not just
+        [eq] *)
+    Definition Interp_APP_rel_reflexive {base_type ident interp_base_type interp_ident} {s d} {R} {H:Reflexive R}
+               (f : @Expr base_type ident (s -> d)) (x : @Expr base_type ident s)
+      : R (@Interp base_type ident interp_base_type interp_ident _ (APP f x))
+          (Interp interp_ident f (Interp interp_ident x))
+      := H _.
+
+    Module var_context.
+      Inductive list {base_type} {var : type base_type -> Type} :=
+      | nil
+      | cons {T t} (gallina_v : T) (v : var t) (ctx : list).
+    End var_context.
+
+    (* cf COQBUG(https://github.com/coq/coq/issues/5448) , COQBUG(https://github.com/coq/coq/issues/6315) , COQBUG(https://github.com/coq/coq/issues/6559) , COQBUG(https://github.com/coq/coq/issues/6534) , https://github.com/mit-plv/fiat-crypto/issues/320 *)
+    Ltac require_same_var n1 n2 :=
+      (*idtac n1 n2;*)
+      let c1 := constr:(fun n1 n2 : Set => ltac:(exact n1)) in
+      let c2 := constr:(fun n1 n2 : Set => ltac:(exact n2)) in
+      (*idtac c1 c2;*)
+      first [ constr_eq c1 c2 | fail 1 "Not the same var:" n1 "and" n2 "(via constr_eq" c1 c2 ")" ].
+    Ltac is_same_var n1 n2 :=
+      match goal with
+      | _ => let check := match goal with _ => require_same_var n1 n2 end in
+             true
+      | _ => false
+      end.
+    Ltac is_underscore v :=
+      let v' := fresh v in
+      let v' := fresh v' in
+      is_same_var v v'.
+    Ltac refresh n fresh_tac :=
+      let n_is_underscore := is_underscore n in
+      let n' := lazymatch n_is_underscore with
+                | true => fresh
+                | false => fresh_tac n
+                end in
+      let n' := fresh_tac n' in
+      n'.
+
+    Ltac type_of_first_argument_of f :=
+      let f_ty := type of f in
+      lazymatch eval hnf in f_ty with
+      | forall x : ?T, _ => T
+      end.
+
+    (** Forms of abstraction in Gallina that our reflective language
+        cannot handle get handled by specializing the code "template"
+        to each particular application of that abstraction. In
+        particular, type arguments (nat, Z, (λ _, nat), etc) get
+        substituted into lambdas and treated as a integral part of
+        primitive operations (such as [@List.app T], [@list_rect (λ _,
+        nat)]).  During reification, we accumulate them in a
+        right-associated tuple, using [tt] as the "nil" base case.
+        When we hit a λ or an identifier, we plug in the template
+        parameters as necessary. *)
+    Ltac require_template_parameter parameter_type :=
+      first [ unify parameter_type Prop
+            | unify parameter_type Set
+            | unify parameter_type Type
+            | lazymatch eval hnf in parameter_type with
+              | forall x : ?T, @?P x
+                => let check := constr:(fun x : T
+                                        => ltac:(require_template_parameter (P x);
+                                                 exact I)) in
+                   idtac
+              end ].
+    Ltac is_template_parameter parameter_type :=
+      is_success_run_tactic ltac:(fun _ => require_template_parameter parameter_type).
+    Ltac plug_template_ctx f template_ctx :=
+      lazymatch template_ctx with
+      | tt => f
+      | (?arg, ?template_ctx')
+        =>
+        let T := type_of_first_argument_of f in
+        let x_is_template_parameter := is_template_parameter T in
+        lazymatch x_is_template_parameter with
+        | true
+          => plug_template_ctx (f arg) template_ctx'
+        | false
+          => constr:(fun x : T
+                     => ltac:(let v := plug_template_ctx (f x) template_ctx in
+                              exact v))
+        end
+      end.
+
+    Ltac reify_in_context base_type ident reify_base_type reify_ident var term value_ctx template_ctx :=
+      let reify_rec_gen term value_ctx template_ctx := reify_in_context base_type ident reify_base_type reify_ident var term value_ctx template_ctx in
+      let reify_rec term := reify_rec_gen term value_ctx template_ctx in
+      let reify_rec_not_head term := reify_rec_gen term value_ctx tt in
+      let do_reify_ident term else_tac
+          := reify_ident
+               term
+               ltac:(fun idc => constr:(@Ident base_type ident var _ idc))
+                      reify_rec
+                      else_tac in
+      let __ := Reify.debug_enter_reify_in_context term in
+      lazymatch value_ctx with
+      | context[@var_context.cons _ _ ?T ?rT term ?v _]
+        => constr:(@Var base_type ident var rT v)
+      | _
+        =>
+        lazymatch term with
+        | match ?b with true => ?t | false => ?f end
+          => let T := type of term in
+             reify_rec (@bool_rect (fun _ => T) t f b)
+        | match ?x with Datatypes.pair a b => @?f a b end
+          => let T := type of term in
+             reify_rec (@prod_rect _ _ (fun _ => T) f x)
+        | match ?x with nil => ?N | cons a b => @?C a b end
+          => let T := type of term in
+             reify_rec (@list_case _ (fun _ => T) N C x)
+        | let x := ?a in ?b
+          => let A := type of a in
+             let T := type of term in
+             let rec_val := match constr:(Set) with
+                            | _ => let v := constr:((fun x : A => b) a) in
+                                   let __ := type of v in (* ensure that the abstraction is well-typed, i.e., that we're not relying on the value of the let to well-type the body *)
+                                   v
+                            | _ => constr:(match a return T with x => b end) (* if we do rely on the body of [x] to well-type [b], then just inline it *)
+                            end in
+             (*let B := lazymatch type of b with forall x, @?B x => B end in*)
+             reify_rec rec_val (*(@Let_In A B a b)*)
+        | @Let_In ?A ?B ?a ?b
+          => let ra := reify_rec a in
+             let rb := reify_rec b in
+             lazymatch rb with
+             | @Abs _ _ _ ?s ?d ?f
+               => constr:(@LetIn base_type ident var s d ra f)
+             | ?rb => let __ := match goal with
+                                | _ => fail 1 "Invalid non-Abs function reification of" b "to" rb
+                                end in
+                      constr:(I : I)
+             end
+        | (fun x : ?T => ?f)
+          =>
+          let x_is_template_parameter := is_template_parameter T in
+          lazymatch x_is_template_parameter with
+          | true
+            =>
+            lazymatch template_ctx with
+            | (?arg, ?template_ctx)
+              => (* we pull a trick with [match] to plug in [arg] without running cbv β *)
+              lazymatch type of term with
+              | forall y, ?P
+                => reify_rec_gen (match arg as y return P with x => f end) value_ctx template_ctx
+              end
+            end
+          | false
+            =>
+            let rT := type.reify reify_base_type base_type T in
+            let not_x := fresh (* could be [refresh x ltac:(fun n => fresh n)] in 8.8; c.f. https://github.com/mit-plv/fiat-crypto/issues/320 and probably COQBUG(https://github.com/coq/coq/issues/6534) *) in
+            let not_x2 := fresh (* could be [refresh not_x ltac:(fun n => fresh n)] in 8.8; c.f. https://github.com/mit-plv/fiat-crypto/issues/320 and probably COQBUG(https://github.com/coq/coq/issues/6534) *) in
+            let not_x3 := fresh (* could be [refresh not_x2 ltac:(fun n => fresh n)] in 8.8; c.f. https://github.com/mit-plv/fiat-crypto/issues/320 and probably COQBUG(https://github.com/coq/coq/issues/6534) *) in
+            (*let __ := match goal with _ => idtac "reify_in_context: λ case:" term "using vars:" not_x not_x2 not_x3 end in*)
+            let rf0 :=
+                constr:(
+                  fun (x : T) (not_x : var rT)
+                  => match f, @var_context.cons base_type var T rT x not_x value_ctx return _ with (* c.f. COQBUG(https://github.com/coq/coq/issues/6252#issuecomment-347041995) for [return _] *)
+                     | not_x2, not_x3
+                       => ltac:(
+                            let f := (eval cbv delta [not_x2] in not_x2) in
+                            let var_ctx := (eval cbv delta [not_x3] in not_x3) in
+                            (*idtac "rec call" f "was" term;*)
+                            let rf := reify_rec_gen f var_ctx template_ctx in
+                            exact rf)
+                     end) in
+            lazymatch rf0 with
+            | (fun _ => ?rf)
+              => constr:(@Abs base_type ident var rT _ rf)
+            | _
+              => (* This will happen if the reified term still
+                    mentions the non-var variable.  By chance, [cbv
+                    delta] strips type casts, which are only places
+                    that I can think of where such dependency might
+                    remain.  However, if this does come up, having a
+                    distinctive error message is much more useful for
+                    debugging than the generic "no matching clause" *)
+              let __ := match goal with
+                        | _ => fail 1 "Failure to eliminate functional dependencies of" rf0
+                        end in
+              constr:(I : I)
+            end
+          end
+        | _
+          =>
+          do_reify_ident
+            term
+            ltac:(
+            fun _
+            =>
+              lazymatch term with
+              | ?f ?x
+                =>
+                let ty := type_of_first_argument_of f in
+                let x_is_template_parameter := is_template_parameter ty in
+                lazymatch x_is_template_parameter with
+                | true
+                  => (* we can't reify things of type [Type], so we save it for later to plug in *)
+                  reify_rec_gen f value_ctx (x, template_ctx)
+                | false
+                  => let rx := reify_rec_gen x value_ctx tt in
+                     let rf := reify_rec_gen f value_ctx template_ctx in
+                     constr:(App (base_type:=base_type) (ident:=ident) (var:=var) rf rx)
+                end
+              | _
+                => let term' := plug_template_ctx term template_ctx in
+                   do_reify_ident
+                     term'
+                     ltac:(fun _
+                           =>
+                             (*let __ := match goal with _ => idtac "Attempting to unfold" term end in*)
+                             let term
+                                 := match constr:(Set) with
+                                    | _ => (eval cbv delta [term] in term) (* might fail, so we wrap it in a match to give better error messages *)
+                                    | _
+                                      => let __ := match goal with
+                                                   | _ => fail 2 "Unrecognized term:" term'
+                                                   end in
+                                         constr:(I : I)
+                                    end in
+                             match constr:(Set) with
+                             | _ => reify_rec term
+                             | _ => let __ := match goal with
+                                              | _ => idtac "Error: Failed to reify" term' "via unfolding";
+                                                     fail 2 "Failed to reify" term' "via unfolding"
+                                              end in
+                                    constr:(I : I)
+                             end)
+              end)
+        end
+      end.
+    Ltac reify base_type ident reify_base_type reify_ident var term :=
+      reify_in_context base_type ident reify_base_type reify_ident var term (@var_context.nil base_type var) tt.
+    Ltac Reify base_type ident reify_base_type reify_ident term :=
+      constr:(fun var : type base_type -> Type
+              => ltac:(let r := reify base_type ident reify_base_type reify_ident var term in
+                       exact r)).
+    Ltac Reify_rhs base_type ident reify_base_type reify_ident base_interp interp_ident _ :=
+      let RHS := lazymatch goal with |- _ = ?RHS => RHS end in
+      let R := Reify base_type ident reify_base_type reify_ident RHS in
+      transitivity (@Interp base_type ident base_interp interp_ident _ R);
+      [ | reflexivity ].
+
+    Module Export Notations.
+      Delimit Scope expr_scope with expr.
+      Delimit Scope Expr_scope with Expr.
+      Delimit Scope expr_pat_scope with expr_pat.
+      Bind Scope expr_scope with expr.
+      Bind Scope Expr_scope with Expr.
+      Infix "@" := App : expr_scope.
+      Infix "@" := APP : Expr_scope.
+      Notation "\ x .. y , f" := (Abs (fun x => .. (Abs (fun y => f%expr)) .. )) : expr_scope.
+      Notation "'λ' x .. y , f" := (Abs (fun x => .. (Abs (fun y => f%expr)) .. )) : expr_scope.
+      Notation "'expr_let' x := A 'in' b" := (LetIn A (fun x => b%expr)) : expr_scope.
+      Notation "'$' x" := (Var x) (at level 10, format "'$' x") : expr_scope.
+      Notation "### x" := (Ident x) : expr_scope.
+    End Notations.
+  End expr.
+  Export expr.Notations.
+  Notation expr := expr.expr.
+
+  Module ident.
+    Local Notation type := (type base.type).
+    Local Notation ttype := type.
+    Module fancy.
+      Section with_base.
+        Let type_base (x : base.type) : type := type.base x.
+        Local Coercion type_base : base.type >-> type.
+        Section with_scope.
+          Import base.type.
+          Notation type := ttype.
+
+          Inductive ident_with_wordmax {log2wordmax : BinInt.Z} : base.type -> base.type -> Set :=
+          | add (imm : BinInt.Z) : ident_with_wordmax (Z * Z) (Z * Z)
+          | addc (imm : BinInt.Z) : ident_with_wordmax (Z * Z * Z) (Z * Z)
+          | sub (imm : BinInt.Z) : ident_with_wordmax (Z * Z) (Z * Z)
+          | subb (imm : BinInt.Z) : ident_with_wordmax (Z * Z * Z) (Z * Z)
+          | mulll : ident_with_wordmax (Z * Z) Z
+          | mullh : ident_with_wordmax (Z * Z) Z
+          | mulhl : ident_with_wordmax (Z * Z) Z
+          | mulhh : ident_with_wordmax (Z * Z) Z
+          | selm : ident_with_wordmax (Z * Z * Z) Z
+          | rshi : BinInt.Z -> ident_with_wordmax (Z * Z) Z
+          .
+
+          Inductive ident : base.type -> base.type -> Set :=
+          | with_wordmax (log2wordmax : BinInt.Z) {s d} (idc : @ident_with_wordmax log2wordmax s d) : ident s d
+          | selc : ident (Z * Z * Z) Z
+          | sell : ident (Z * Z * Z) Z
+          | addm : ident (Z * Z * Z) Z
+          .
+
+          Section interp_with_wordmax.
+            Context (log2wordmax : BinInt.Z).
+            Let wordmax := 2 ^ log2wordmax.
+            Let half_bits := log2wordmax / 2.
+            Let wordmax_half_bits := 2 ^ half_bits.
+
+            Local Notation low x := (Z.land x (wordmax_half_bits - 1)).
+            Local Notation high x := (x >> half_bits).
+            Local Notation shift x imm := ((x << imm) mod wordmax).
+
+            Definition interp_with_wordmax {s d} (idc : @ident_with_wordmax log2wordmax s d) : base.interp s -> base.interp d :=
+              match idc with
+              | add imm => fun x => Z.add_get_carry_full wordmax (fst x) (shift (snd x) imm)
+              | addc imm => fun x => Z.add_with_get_carry_full wordmax (fst (fst x)) (snd (fst x)) (shift (snd x) imm)
+              | sub imm => fun x => Z.sub_get_borrow_full wordmax (fst x) (shift (snd x) imm)
+              | subb imm => fun x => Z.sub_with_get_borrow_full wordmax (fst (fst x)) (snd (fst x)) (shift (snd x) imm)
+              | mulll => fun x => low (fst x) * low (snd x)
+              | mullh => fun x => low (fst x) * high (snd x)
+              | mulhl => fun x => high (fst x) * low (snd x)
+              | mulhh => fun x => high (fst x) * high (snd x)
+              | rshi n => fun x => Z.rshi wordmax (fst x) (snd x) n
+              | selm => fun x => Z.zselect (Z.cc_m wordmax (fst (fst x))) (snd (fst x)) (snd x)
+              end.
+          End interp_with_wordmax.
+
+          Definition interp {s d} (idc : @ident s d) : base.interp s -> base.interp d :=
+            match idc with
+            | with_wordmax lwm s d idc => interp_with_wordmax lwm idc
+            | selc => fun x => Z.zselect (fst (fst x)) (snd (fst x)) (snd x)
+            | sell => fun x => Z.zselect (Z.land (fst (fst x)) 1) (snd (fst x)) (snd x)
+            | addm => fun x => Z.add_modulo (fst (fst x)) (snd (fst x)) (snd x)
+            end.
+        End with_scope.
+      End with_base.
+      Global Coercion with_wordmax : ident_with_wordmax >-> ident.
+      Global Arguments interp_with_wordmax {_ s d} idc.
+      Global Arguments interp {s d} idc.
+    End fancy.
+
+    Section with_base.
+      Let type_base (x : base.type) : type := type.base x.
+      Local Coercion type_base : base.type >-> type.
+      Section with_scope.
+        Import base.type.
+        Notation type := ttype.
+        (* N.B. [ident] must have essentially flat structure for the
+           python script constructing [pattern.ident] to work *)
+        Inductive ident : type -> Type :=
+        | Literal {t:base.type.base} (v : base.interp t) : ident t
+        | Nat_succ : ident (nat -> nat)
+        | Nat_pred : ident (nat -> nat)
+        | Nat_max : ident (nat -> nat -> nat)
+        | Nat_mul : ident (nat -> nat -> nat)
+        | Nat_add : ident (nat -> nat -> nat)
+        | Nat_sub : ident (nat -> nat -> nat)
+        | nil {t} : ident (list t)
+        | cons {t:base.type} : ident (t -> list t -> list t)
+        | pair {A B:base.type} : ident (A -> B -> A * B)
+        | fst {A B} : ident (A * B -> A)
+        | snd {A B} : ident (A * B -> B)
+        | prod_rect {A B T:base.type} : ident ((A -> B -> T) -> A * B -> T)
+        | bool_rect {T:base.type} : ident ((unit -> T) -> (unit -> T) -> bool -> T)
+        | nat_rect {P:base.type} : ident ((unit -> P) -> (nat -> P -> P) -> nat -> P)
+        | nat_rect_arrow {P Q:base.type} : ident ((P -> Q) -> (nat -> (P -> Q) -> (P -> Q)) -> nat -> P -> Q)
+        | list_rect {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P -> P) -> list A -> P)
+        | list_case {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P) -> list A -> P)
+        | List_length {T} : ident (list T -> nat)
+        | List_seq : ident (nat -> nat -> list nat)
+        | List_firstn {A:base.type} : ident (nat -> list A -> list A)
+        | List_skipn {A:base.type} : ident (nat -> list A -> list A)
+        | List_repeat {A:base.type} : ident (A -> nat -> list A)
+        | List_combine {A B} : ident (list A -> list B -> list (A * B))
+        | List_map {A B:base.type} : ident ((A -> B) -> list A -> list B)
+        | List_app {A} : ident (list A -> list A -> list A)
+        | List_rev {A} : ident (list A -> list A)
+        | List_flat_map {A B:base.type} : ident ((A -> (list B)) -> list A -> (list B))
+        | List_partition {A:base.type} : ident ((A -> bool) -> list A -> (list A * list A))
+        | List_fold_right {A B:base.type} : ident ((B -> A -> A) -> A -> list B -> A)
+        | List_update_nth {T:base.type} : ident (nat -> (T -> T) -> list T -> list T)
+        | List_nth_default {T:base.type} : ident (T -> list T -> nat -> T)
+        | Z_add : ident (Z -> Z -> Z)
+        | Z_mul : ident (Z -> Z -> Z)
+        | Z_pow : ident (Z -> Z -> Z)
+        | Z_sub : ident (Z -> Z -> Z)
+        | Z_opp : ident (Z -> Z)
+        | Z_div : ident (Z -> Z -> Z)
+        | Z_modulo : ident (Z -> Z -> Z)
+        | Z_log2 : ident (Z -> Z)
+        | Z_log2_up : ident (Z -> Z)
+        | Z_eqb : ident (Z -> Z -> bool)
+        | Z_leb : ident (Z -> Z -> bool)
+        | Z_geb : ident (Z -> Z -> bool)
+        | Z_of_nat : ident (nat -> Z)
+        | Z_to_nat : ident (Z -> nat)
+        | Z_shiftr : ident (Z -> Z -> Z)
+        | Z_shiftl : ident (Z -> Z -> Z)
+        | Z_land : ident (Z -> Z -> Z)
+        | Z_lor : ident (Z -> Z -> Z)
+        | Z_bneg : ident (Z -> Z)
+        | Z_lnot_modulo : ident (Z -> Z -> Z)
+        | Z_mul_split : ident (Z -> Z -> Z -> Z * Z)
+        | Z_add_get_carry : ident (Z -> Z -> Z -> (Z * Z))
+        | Z_add_with_carry : ident (Z -> Z -> Z -> Z)
+        | Z_add_with_get_carry : ident (Z -> Z -> Z -> Z -> (Z * Z))
+        | Z_sub_get_borrow : ident (Z -> Z -> Z -> (Z * Z))
+        | Z_sub_with_get_borrow : ident (Z -> Z -> Z -> Z -> (Z * Z))
+        | Z_zselect : ident (Z -> Z -> Z -> Z)
+        | Z_add_modulo : ident (Z -> Z -> Z -> Z)
+        | Z_rshi : ident (Z -> Z -> Z -> Z -> Z)
+        | Z_cc_m : ident (Z -> Z -> Z)
+        | Z_cast (range : zrange) : ident (Z -> Z)
+        | Z_cast2 (range : zrange * zrange) : ident ((Z * Z) -> (Z * Z))
+        | fancy_add (log2wordmax : BinInt.Z) (imm : BinInt.Z) : ident (Z * Z -> Z * Z)
+        | fancy_addc (log2wordmax : BinInt.Z) (imm : BinInt.Z) : ident (Z * Z * Z -> Z * Z)
+        | fancy_sub (log2wordmax : BinInt.Z) (imm : BinInt.Z) : ident (Z * Z -> Z * Z)
+        | fancy_subb (log2wordmax : BinInt.Z) (imm : BinInt.Z) : ident (Z * Z * Z -> Z * Z)
+        | fancy_mulll (log2wordmax : BinInt.Z) : ident (Z * Z -> Z)
+        | fancy_mullh (log2wordmax : BinInt.Z) : ident (Z * Z -> Z)
+        | fancy_mulhl (log2wordmax : BinInt.Z) : ident (Z * Z -> Z)
+        | fancy_mulhh (log2wordmax : BinInt.Z) : ident (Z * Z -> Z)
+        | fancy_rshi (log2wordmax : BinInt.Z) : BinInt.Z -> ident (Z * Z -> Z)
+        | fancy_selc : ident (Z * Z * Z -> Z)
+        | fancy_selm (log2wordmax : BinInt.Z) : ident (Z * Z * Z -> Z)
+        | fancy_sell : ident (Z * Z * Z -> Z)
+        | fancy_addm : ident (Z * Z * Z -> Z)
+        .
+
+        Global Arguments Z_cast2 _%zrange_scope.
+
+        Definition to_fancy {s d : base.type} (idc : ident (s -> d)) : option (fancy.ident s d)
+          := match idc in ident t return option match t with
+                                                | type.base s -> type.base d => fancy.ident s d
+                                                | _ => Datatypes.unit
+                                                end%etype with
+             | fancy_add log2wordmax imm => Some (fancy.with_wordmax log2wordmax (fancy.add imm))
+             | fancy_addc log2wordmax imm => Some (fancy.with_wordmax log2wordmax (fancy.addc imm))
+             | fancy_sub log2wordmax imm => Some (fancy.with_wordmax log2wordmax (fancy.sub imm))
+             | fancy_subb log2wordmax imm => Some (fancy.with_wordmax log2wordmax (fancy.subb imm))
+             | fancy_mulll log2wordmax => Some (fancy.with_wordmax log2wordmax fancy.mulll)
+             | fancy_mullh log2wordmax => Some (fancy.with_wordmax log2wordmax fancy.mullh)
+             | fancy_mulhl log2wordmax => Some (fancy.with_wordmax log2wordmax fancy.mulhl)
+             | fancy_mulhh log2wordmax => Some (fancy.with_wordmax log2wordmax fancy.mulhh)
+             | fancy_rshi log2wordmax x => Some (fancy.with_wordmax log2wordmax (fancy.rshi x))
+             | fancy_selc => Some fancy.selc
+             | fancy_selm log2wordmax => Some (fancy.with_wordmax log2wordmax fancy.selm)
+             | fancy_sell => Some fancy.sell
+             | fancy_addm => Some fancy.addm
+             | _ => None
+             end.
+      End with_scope.
+
+      Section gen.
+        Context (cast_outside_of_range : zrange -> BinInt.Z -> BinInt.Z).
+
+        Definition is_more_pos_than_neg (r : zrange) (v : BinInt.Z) : bool
+          := ((Z.abs (lower r) <? Z.abs (upper r)) (* if more of the range is above 0 than below 0 *)
+              || ((lower r =? upper r) && (0 <=? lower r))
+              || ((Z.abs (lower r) =? Z.abs (upper r)) && (0 <=? v))).
+
+        (** We ensure that [ident.cast] is symmetric under [Z.opp], as
+            this makes some rewrite rules much, much easier to
+            prove. *)
+        Let cast_outside_of_range' (r : zrange) (v : BinInt.Z) : BinInt.Z
+          := ((cast_outside_of_range r v - lower r) mod (upper r - lower r + 1)) + lower r.
+
+        Definition cast (r : zrange) (x : BinInt.Z)
+          := let r := ZRange.normalize r in
+             if (lower r <=? x) && (x <=? upper r)
+             then x
+             else if is_more_pos_than_neg r x
+                  then cast_outside_of_range' r x
+                  else -cast_outside_of_range' (-r) (-x).
+
+        Local Notation wordmax log2wordmax := (2 ^ log2wordmax).
+        Local Notation half_bits log2wordmax := (log2wordmax / 2).
+        Local Notation wordmax_half_bits log2wordmax := (2 ^ (half_bits log2wordmax)).
+
+        Local Notation low log2wordmax x := (Z.land x ((wordmax_half_bits log2wordmax) - 1)).
+        Local Notation high log2wordmax x := (x >> (half_bits log2wordmax)).
+        Local Notation shift log2wordmax x imm := ((x << imm) mod (wordmax log2wordmax)).
+
+        (** Interpret identifiers where the behavior of [Z_cast] on a
+            value that does not fit in the range is given by a context
+            variable.  (This allows us to treat [Z_cast] as "undefined
+            behavior" when the value doesn't fit in the range by
+            quantifying over all possible interpretations. *)
+        Definition gen_interp {t} (idc : ident t) : type.interp base.interp t
+          := match idc in ident t return type.interp base.interp t with
+             | Literal _ v => v
+             | Nat_succ => Nat.succ
+             | Nat_pred => Nat.pred
+             | Nat_max => Nat.max
+             | Nat_mul => Nat.mul
+             | Nat_add => Nat.add
+             | Nat_sub => Nat.sub
+             | nil t => Datatypes.nil
+             | cons t => Datatypes.cons
+             | pair A B => Datatypes.pair
+             | fst A B => Datatypes.fst
+             | snd A B => Datatypes.snd
+             | prod_rect A B T => fun f '((a, b) : base.interp A * base.interp B) => f a b
+             | bool_rect T
+               => fun t f => Datatypes.bool_rect _ (t tt) (f tt)
+             | nat_rect P
+               => fun O_case S_case => Datatypes.nat_rect _ (O_case tt) S_case
+             | nat_rect_arrow P Q
+               => fun O_case S_case => Datatypes.nat_rect _ O_case S_case
+             | list_rect A P
+               => fun N_case C_case => Datatypes.list_rect _ (N_case tt) C_case
+             | list_case A P
+               => fun N_case C_case => ListUtil.list_case _ (N_case tt) C_case
+             | List_length T => @List.length _
+             | List_seq => List.seq
+             | List_firstn A => @List.firstn _
+             | List_skipn A => @List.skipn _
+             | List_repeat A => @repeat _
+             | List_combine A B => @List.combine _ _
+             | List_map A B => @List.map _ _
+             | List_app A => @List.app _
+             | List_rev A => @List.rev _
+             | List_flat_map A B => @List.flat_map _ _
+             | List_partition A => @List.partition _
+             | List_fold_right A B => @List.fold_right _ _
+             | List_update_nth T => update_nth
+             | List_nth_default T => @nth_default _
+             | Z_add => Z.add
+             | Z_mul => Z.mul
+             | Z_pow => Z.pow
+             | Z_sub => Z.sub
+             | Z_opp => Z.opp
+             | Z_div => Z.div
+             | Z_modulo => Z.modulo
+             | Z_eqb => Z.eqb
+             | Z_leb => Z.leb
+             | Z_geb => Z.geb
+             | Z_log2 => Z.log2
+             | Z_log2_up => Z.log2_up
+             | Z_of_nat => Z.of_nat
+             | Z_to_nat => Z.to_nat
+             | Z_shiftr => Z.shiftr
+             | Z_shiftl => Z.shiftl
+             | Z_land => Z.land
+             | Z_lor => Z.lor
+             | Z_mul_split => Z.mul_split
+             | Z_add_get_carry => Z.add_get_carry_full
+             | Z_add_with_carry => Z.add_with_carry
+             | Z_add_with_get_carry => Z.add_with_get_carry_full
+             | Z_sub_get_borrow => Z.sub_get_borrow_full
+             | Z_sub_with_get_borrow => Z.sub_with_get_borrow_full
+             | Z_zselect => Z.zselect
+             | Z_add_modulo => Z.add_modulo
+             | Z_bneg => Z.bneg
+             | Z_lnot_modulo => Z.lnot_modulo
+             | Z_rshi => Z.rshi
+             | Z_cc_m => Z.cc_m
+             | Z_cast r => cast r
+             | Z_cast2 (r1, r2) => fun '(x1, x2) => (cast r1 x1, cast r2 x2)
+             | fancy_add _ _ as idc
+             | fancy_addc _ _ as idc
+             | fancy_sub _ _ as idc
+             | fancy_subb _ _ as idc
+             | fancy_mulll _ as idc
+             | fancy_mullh _ as idc
+             | fancy_mulhl _ as idc
+             | fancy_mulhh _ as idc
+             | fancy_rshi _ _ as idc
+             | fancy_selc as idc
+             | fancy_selm _ as idc
+             | fancy_sell as idc
+             | fancy_addm as idc
+               => fancy.interp (invert_Some (to_fancy idc))
+             end.
+      End gen.
+
+      Definition cast_outside_of_range (r : zrange) (v : BinInt.Z) : BinInt.Z.
+      Proof. exact v. Qed.
+    End with_base.
+
+    (** Interpret identifiers where [Z_cast] is an opaque identity
+        function when the value is not inside the range *)
+    Notation interp := (@gen_interp cast_outside_of_range).
+    Notation LiteralUnit := (@Literal base.type.unit).
+    Notation LiteralZ := (@Literal base.type.Z).
+    Notation LiteralBool := (@Literal base.type.bool).
+    Notation LiteralNat := (@Literal base.type.nat).
+
+    (** TODO: MOVE ME? *)
+    Module Thunked.
+      Definition bool_rect P (t f : Datatypes.unit -> P) (b : bool) : P
+        := Datatypes.bool_rect (fun _ => P) (t tt) (f tt) b.
+      Definition list_rect {A} P (N : Datatypes.unit -> P) (C : A -> list A -> P -> P) (ls : list A) : P
+        := Datatypes.list_rect (fun _ => P) (N tt) C ls.
+      Definition list_case {A} P (N : Datatypes.unit -> P) (C : A -> list A -> P) (ls : list A) : P
+        := ListUtil.list_case (fun _ => P) (N tt) C ls.
+      Definition nat_rect P (O_case : unit -> P) (S_case : nat -> P -> P) (n : nat) : P
+        := Datatypes.nat_rect (fun _ => P) (O_case tt) S_case n.
+    End Thunked.
+
+    Ltac require_primitive_const term :=
+      lazymatch term with
+      | S ?n => require_primitive_const n
+      | O => idtac
+      | true => idtac
+      | false => idtac
+      | tt => idtac
+      | Z0 => idtac
+      | Zpos ?p => require_primitive_const p
+      | Zneg ?p => require_primitive_const p
+      | xI ?p => require_primitive_const p
+      | xO ?p => require_primitive_const p
+      | xH => idtac
+      | ?term => fail 0 "Not a known const:" term
+      end.
+    Ltac is_primitive_const term :=
+      match constr:(Set) with
+      | _ => let check := match goal with
+                          | _ => require_primitive_const term
+                          end in
+             true
+      | _ => false
+      end.
+
+    Ltac reify
+         term
+         then_tac
+         reify_rec
+         else_tac :=
+      (*let __ := match goal with _ => idtac "attempting to reify_op" term end in*)
+      let term_is_primitive_const := is_primitive_const term in
+      lazymatch term_is_primitive_const with
+      | true
+        =>
+        let T := type of term in
+        let rT := base.reify_base T in
+        then_tac (@ident.Literal rT term)
+      | false
+        =>
+        lazymatch term with
+        | Nat.succ => then_tac Nat_succ
+        | Nat.add => then_tac Nat_add
+        | Nat.sub => then_tac Nat_sub
+        | Nat.mul => then_tac Nat_mul
+        | Nat.max => then_tac Nat_max
+        | Nat.pred => then_tac Nat_pred
+        | S => then_tac Nat_succ
+        | @Datatypes.nil ?T
+          => let rT := base.reify T in
+             then_tac (@ident.nil rT)
+        | @Datatypes.cons ?T
+          => let rT := base.reify T in
+             then_tac (@ident.cons rT)
+        | @Datatypes.fst ?A ?B
+          => let rA := base.reify A in
+             let rB := base.reify B in
+             then_tac (@ident.fst rA rB)
+        | @Datatypes.snd ?A ?B
+          => let rA := base.reify A in
+             let rB := base.reify B in
+             then_tac (@ident.snd rA rB)
+        | @Datatypes.pair ?A ?B
+          => let rA := base.reify A in
+             let rB := base.reify B in
+             then_tac (@ident.pair rA rB)
+        | @Datatypes.bool_rect ?T0 ?Ptrue ?Pfalse
+          => lazymatch (eval cbv beta in T0) with
+            | fun _ => ?T => reify_rec (@Thunked.bool_rect T (fun _ : Datatypes.unit => Ptrue) (fun _ : Datatypes.unit => Pfalse))
+            | T0 => else_tac ()
+            | ?T' => reify_rec (@Datatypes.bool_rect T' Ptrue Pfalse)
+            end
+        | @Thunked.bool_rect ?T
+          => let rT := base.reify T in
+             then_tac (@ident.bool_rect rT)
+        | @Datatypes.prod_rect ?A ?B ?T0
+          => lazymatch (eval cbv beta in T0) with
+            | fun _ => ?T
+              => let rA := base.reify A in
+                let rB := base.reify B in
+                let rT := base.reify T in
+                then_tac (@ident.prod_rect rA rB rT)
+            | T0 => else_tac ()
+            | ?T' => reify_rec (@Datatypes.prod_rect A B T')
+            end
+        | @Datatypes.nat_rect ?T0 ?P0
+          => lazymatch (eval cbv beta in T0) with
+             | fun _ => _ -> _ => else_tac ()
+             | fun _ => ?T => reify_rec (@Thunked.nat_rect T (fun _ : Datatypes.unit => P0))
+             | T0 => else_tac ()
+             | ?T' => reify_rec (@Datatypes.nat_rect T' P0)
+             end
+        | @Datatypes.nat_rect ?T0
+          => lazymatch (eval cbv beta in T0) with
+            | (fun _ => ?P -> ?Q)
+              => let rP := base.reify P in
+                let rQ := base.reify Q in
+                then_tac (@ident.nat_rect_arrow rP rQ)
+             | T0 => else_tac ()
+             | ?T' => reify_rec (@Datatypes.nat_rect T')
+            end
+        | @Thunked.nat_rect ?T
+          => let rT := base.reify T in
+             then_tac (@ident.nat_rect rT)
+        | @Datatypes.list_rect ?A ?T0 ?Pnil
+          => lazymatch (eval cbv beta in T0) with
+            | fun _ => ?T => reify_rec (@Thunked.list_rect A T (fun _ : Datatypes.unit => Pnil))
+            | T0 => else_tac ()
+            | ?T' => reify_rec (@Datatypes.list_rect A T' Pnil)
+            end
+        | @Thunked.list_rect ?A ?T
+          => let rA := base.reify A in
+             let rT := base.reify T in
+             then_tac (@ident.list_rect rA rT)
+        | @ListUtil.list_case ?A ?T0 ?Pnil
+          => lazymatch (eval cbv beta in T0) with
+            | fun _ => ?T => reify_rec (@Thunked.list_case A T (fun _ : Datatypes.unit => Pnil))
+            | T0 => else_tac ()
+            | ?T' => reify_rec (@ListUtil.list_case A T' Pnil)
+            end
+        | @Thunked.list_case ?A ?T
+          => let rA := base.reify A in
+             let rT := base.reify T in
+             then_tac (@ident.list_case rA rT)
+        | @List.length ?A =>
+          let rA := base.reify A in
+          then_tac (@ident.List_length rA)
+        | List.seq => then_tac ident.List_seq
+        | @List.firstn ?A
+          => let rA := base.reify A in
+             then_tac (@ident.List_firstn rA)
+        | @List.skipn ?A
+          => let rA := base.reify A in
+             then_tac (@ident.List_skipn rA)
+        | @repeat ?A
+          => let rA := base.reify A in
+             then_tac (@ident.List_repeat rA)
+        | @combine ?A ?B
+          => let rA := base.reify A in
+             let rB := base.reify B in
+             then_tac (@ident.List_combine rA rB)
+        | @List.map ?A ?B
+          => let rA := base.reify A in
+             let rB := base.reify B in
+             then_tac (@ident.List_map rA rB)
+        | @List.flat_map ?A ?B
+          => let rA := base.reify A in
+             let rB := base.reify B in
+             then_tac (@ident.List_flat_map rA rB)
+        | @List.partition ?A
+          => let rA := base.reify A in
+             then_tac (@ident.List_partition rA)
+        | @List.app ?A
+          => let rA := base.reify A in
+             then_tac (@ident.List_app rA)
+        | @List.rev ?A
+          => let rA := base.reify A in
+             then_tac (@ident.List_rev rA)
+        | @List.fold_right ?A ?B
+          => let rA := base.reify A in
+             let rB := base.reify B in
+             then_tac (@ident.List_fold_right rA rB)
+        | @update_nth ?T
+          => let rT := base.reify T in
+             then_tac (@ident.List_update_nth rT)
+        | @List.nth_default ?T
+          => let rT := base.reify T in
+             then_tac (@ident.List_nth_default rT)
+        | Z.add => then_tac ident.Z_add
+        | Z.mul => then_tac ident.Z_mul
+        | Z.pow => then_tac ident.Z_pow
+        | Z.sub => then_tac ident.Z_sub
+        | Z.opp => then_tac ident.Z_opp
+        | Z.div => then_tac ident.Z_div
+        | Z.modulo => then_tac ident.Z_modulo
+        | Z.eqb => then_tac ident.Z_eqb
+        | Z.leb => then_tac ident.Z_leb
+        | Z.geb => then_tac ident.Z_geb
+        | Z.log2 => then_tac ident.Z_log2
+        | Z.log2_up => then_tac ident.Z_log2_up
+        | Z.shiftl => then_tac ident.Z_shiftl
+        | Z.shiftr => then_tac ident.Z_shiftr
+        | Z.land => then_tac ident.Z_land
+        | Z.lor => then_tac ident.Z_lor
+        | Z.bneg => then_tac ident.Z_bneg
+        | Z.lnot_modulo => then_tac ident.Z_lnot_modulo
+        | Z.of_nat => then_tac ident.Z_of_nat
+        | Z.to_nat => then_tac ident.Z_to_nat
+        | Z.mul_split => then_tac ident.Z_mul_split
+        | Z.add_get_carry_full => then_tac ident.Z_add_get_carry
+        | Z.add_with_carry => then_tac ident.Z_add_with_carry
+        | Z.add_with_get_carry_full => then_tac ident.Z_add_with_get_carry
+        | Z.sub_get_borrow_full => then_tac ident.Z_sub_get_borrow
+        | Z.sub_with_get_borrow_full => then_tac ident.Z_sub_with_get_borrow
+        | Z.zselect => then_tac ident.Z_zselect
+        | Z.add_modulo => then_tac ident.Z_add_modulo
+        | Z.rshi => then_tac ident.Z_rshi
+        | Z.cc_m => then_tac ident.Z_cc_m
+        | _ => else_tac ()
+        end
+      end.
+
+    Definition reify_list {var} {t} (ls : list (@expr.expr base.type ident var (type.base t))) : @expr.expr base.type ident var (type.base (base.type.list t))
+      := Datatypes.list_rect
+           (fun _ => _)
+           (expr.Ident ident.nil)
+           (fun x _ xs => expr.Ident ident.cons @ x @ xs)%expr
+           ls.
+
+    Fixpoint smart_Literal {var} {t:base.type} : base.interp t -> @expr.expr base.type ident var (type.base t)
+      := match t with
+         | base.type.type_base t => fun v => expr.Ident (ident.Literal v)
+         | base.type.prod A B
+           => fun '((a, b) : base.interp A * base.interp B)
+              => expr.Ident ident.pair @ (@smart_Literal var A a) @ (@smart_Literal var B b)
+         | base.type.list A
+           => fun v : list (base.interp A)
+              => reify_list (List.map (@smart_Literal var A) v)
+         end%expr.
+
+    Module Export Notations.
+      Delimit Scope ident_scope with ident.
+      Bind Scope ident_scope with ident.
+      Global Arguments expr.Ident {base_type%type ident%function var%function t%etype} idc%ident.
+      Notation "## x" := (Literal x) (only printing) : ident_scope.
+      Notation "## x" := (Literal (t:=base.reify_base_type_of x) x) (only parsing) : ident_scope.
+      Notation "## x" := (expr.Ident (Literal x)) (only printing) : expr_scope.
+      Notation "## x" := (smart_Literal (t:=base.reify_type_of x) x) (only parsing) : expr_scope.
+      Notation "# x" := (expr.Ident x) : expr_pat_scope.
+      Notation "# x" := (@expr.Ident base.type _ _ _ x) : expr_scope.
+      Notation "x @ y" := (expr.App x%expr_pat y%expr_pat) : expr_pat_scope.
+      Notation "( x , y , .. , z )" := (expr.App (expr.App (#pair) .. (expr.App (expr.App (#pair) x%expr) y%expr) .. ) z%expr) : expr_scope.
+      Notation "( x , y , .. , z )" := (expr.App (expr.App (#pair)%expr_pat .. (expr.App (expr.App (#pair)%expr_pat x%expr_pat) y%expr_pat) .. ) z%expr_pat) : expr_pat_scope.
+      Notation "x :: y" := (#cons @ x @ y)%expr : expr_scope.
+      Notation "[ ]" := (#nil)%expr : expr_scope.
+      Notation "x :: y" := (#cons @ x @ y)%expr_pat : expr_pat_scope.
+      Notation "[ ]" := (#nil)%expr_pat : expr_pat_scope.
+      Notation "[ x ]" := (x :: [])%expr : expr_scope.
+      Notation "[ x ; y ; .. ; z ]" := (#cons @ x @ (#cons @ y @ .. (#cons @ z @ #nil) ..))%expr : expr_scope.
+      Notation "ls [[ n ]]"
+        := ((#(List_nth_default) @ _ @ ls @ #(Literal n%nat))%expr)
+           : expr_scope.
+      Notation "xs ++ ys" := (#List_app @ xs @ ys)%expr : expr_scope.
+      Notation "x - y" := (#Z_sub @ x @ y)%expr : expr_scope.
+      Notation "x + y" := (#Z_add @ x @ y)%expr : expr_scope.
+      Notation "x / y" := (#Z_div @ x @ y)%expr : expr_scope.
+      Notation "x * y" := (#Z_mul @ x @ y)%expr : expr_scope.
+      Notation "x >> y" := (#Z_shiftr @ x @ y)%expr : expr_scope.
+      Notation "x << y" := (#Z_shiftl @ x @ y)%expr : expr_scope.
+      Notation "x &' y" := (#Z_land @ x @ y)%expr : expr_scope.
+      Notation "x || y" := (#Z_lor @ x @ y)%expr : expr_scope.
+      Notation "x 'mod' y" := (#Z_modulo @ x @ y)%expr : expr_scope.
+      Notation "- x" := (#Z_opp @ x)%expr : expr_scope.
+      Global Arguments gen_interp _ _ !_.
+
+      Global Arguments ident.Z_cast2 _%zrange_scope.
+    End Notations.
+  End ident.
+  Export ident.Notations.
+  Notation ident := ident.ident.
+
+  Global Strategy -1000 [expr.Interp expr.interp type.interp base.interp base.base_interp ident.gen_interp].
+  Ltac reify var term :=
+    expr.reify base.type ident ltac:(base.reify) ident.reify var term.
+  Ltac Reify term :=
+    expr.Reify base.type ident ltac:(base.reify) ident.reify term.
+  Ltac Reify_rhs _ :=
+    expr.Reify_rhs base.type ident ltac:(base.reify) ident.reify (@base.interp) (@ident.interp) ().
+
+  Module Import invert_expr.
+    Module ident.
+      Definition invert_Literal_cps {t} (idc : ident t) : ~> option (type.interp base.interp t)
+        := fun T => match idc with
+                    | ident.Literal _ n => fun k => k (Some n)
+                    | _ => fun k => k None
+                    end.
+
+      Definition invert_Literal {t} (idc : ident t) : option (type.interp base.interp t)
+        := match idc with
+           | ident.Literal _ n => Some n
+           | _ => None
+           end.
+    End ident.
+
+    Section with_var_gen.
+      Context {base_type} {ident var : type base_type -> Type}.
+      Local Notation expr := (@expr base_type ident var).
+      Local Notation if_arrow f t
+        := (match t return Type with
+            | type.arrow s d => f s d
+            | type.base _ => unit
+            end) (only parsing).
+      Definition invert_Ident {t} (e : expr t)
+        : option (ident t)
+        := match e with
+           | expr.Ident t idc => Some idc
+           | _ => None
+           end.
+      Definition invert_App {t} (e : expr t)
+        : option { s : _ & expr (s -> t) * expr s }%type
+        := match e with
+           | expr.App A B f x => Some (existT _ A (f, x))
+           | _ => None
+           end.
+      Definition invert_Abs {s d} (e : expr (s -> d))
+        : option (var s -> expr d)%type
+        := match e in expr.expr t return option (if_arrow (fun s d => var s -> expr d) t) with
+           | expr.Abs s d f => Some f
+           | _ => None
+           end.
+      Definition invert_LetIn {t} (e : expr t)
+        : option { s : _ & expr s * (var s -> expr t) }%type
+        := match e with
+           | expr.LetIn A B x f => Some (existT _ A (x, f))
+           | _ => None
+           end.
+      Definition invert_App2 {t} (e : expr t)
+        : option { ss' : _ & expr (fst ss' -> snd ss' -> t) * expr (fst ss') * expr (snd ss') }%type
+        := (e <- invert_App e;
+              let '(existT s' (f', x')) := e in
+              f' <- invert_App f';
+                let '(existT s (f, x)) := f' in
+                Some (existT _ (s, s') (f, x, x')))%option.
+      Definition invert_AppIdent {t} (e : expr t)
+        : option { s : _ & ident (s -> t) * expr s }%type
+        := (e <- invert_App e;
+              let '(existT s (f, x)) := e in
+              f' <- invert_Ident f;
+                Some (existT _ s (f', x)))%option.
+      Definition invert_AppIdent2 {t} (e : expr t)
+        : option { ss' : _ & ident (fst ss' -> snd ss' -> t) * expr (fst ss') * expr (snd ss') }%type
+        := (e <- invert_App2 e;
+              let '(existT ss' (f, x, x')) := e in
+              f' <- invert_Ident f;
+                Some (existT _ ss' (f', x, x')))%option.
+      Definition invert_Var {t} (e : expr t)
+        : option (var t)
+        := match e with
+           | expr.Var t v => Some v
+           | _ => None
+           end.
+
+      Fixpoint App_curried {t} : expr t -> type.for_each_lhs_of_arrow expr t -> expr (type.base (type.final_codomain t))
+        := match t with
+           | type.base t => fun e _ => e
+           | type.arrow s d => fun e x => @App_curried d (e @ (fst x)) (snd x)
+           end.
+      Fixpoint smart_App_curried {t} (e : expr t) : type.for_each_lhs_of_arrow var t -> expr (type.base (type.final_codomain t))
+        := match e in expr.expr t return type.for_each_lhs_of_arrow var t -> expr (type.base (type.final_codomain t)) with
+           | expr.Abs s d f
+             => fun v => @smart_App_curried d (f (fst v)) (snd v)
+           | e
+             => fun v => @App_curried _ e (type.map_for_each_lhs_of_arrow (fun _ v => expr.Var v) v)
+           end.
+      Fixpoint invert_App_curried {t} (e : expr t)
+        : type.for_each_lhs_of_arrow expr t -> { t' : _ & expr t' * type.for_each_lhs_of_arrow expr t' }%type
+        := match e in expr.expr t return type.for_each_lhs_of_arrow expr t -> { t' : _ & expr t' * type.for_each_lhs_of_arrow expr t' }%type with
+           | expr.App s d f x
+             => fun args
+                => @invert_App_curried _ f (x, args)
+           | e => fun args => existT _ _ (e, args)
+           end.
+      Definition invert_AppIdent_curried {t} (e : expr t)
+        : option { t' : _ & ident t' * type.for_each_lhs_of_arrow expr t' }%type
+        := match t return expr t -> _ with
+           | type.base _ => fun e => let 'existT t (f, args) := invert_App_curried e tt in
+                                     (idc <- invert_Ident f;
+                                        Some (existT _ t (idc, args)))%option
+           | _ => fun _ => None
+           end e.
+    End with_var_gen.
+
+    Section with_var.
+      Context {var : type base.type -> Type}.
+      Local Notation expr := (@expr base.type ident var).
+      Local Notation try_transportP P := (@type.try_transport base.type (@base.try_make_transport_cps) P _ _).
+      Local Notation try_transport := (try_transportP _).
+      Let type_base (v : base.type) : type.type base.type := type.base v.
+      Coercion type_base : base.type >-> type.type.
+
+      Definition invert_Z_opp {t} (e : expr t)
+        : option (expr t)
+        := match e in expr.expr t return option (expr t) with
+           | expr.App (type.base base.type.Z) (type.base base.type.Z) (#ident.Z_opp) v => Some v
+           | _ => None
+           end%expr_pat%expr.
+
+      Definition invert_Z_cast (e : expr base.type.Z)
+        : option (zrange * expr base.type.Z)
+        := match e with
+           | expr.App (type.base base.type.Z) _ (#(ident.Z_cast r)) v => Some (r, v)
+           | _ => None
+           end%core%expr_pat%expr.
+
+      Definition invert_Z_cast2 (e : expr (base.type.Z * base.type.Z))
+        : option ((zrange * zrange) * expr (base.type.Z * base.type.Z))
+        := match e with
+           | expr.App (type.base (base.type.Z * base.type.Z)) _ (#(ident.Z_cast2 r)) v => Some (r, v)
+           | _ => None
+           end%etype%core%expr_pat%expr.
+
+      Definition invert_pair {A B} (e : expr (A * B))
+        : option (expr A * expr B)
+        := match e with
+           | (a, b)
+             => a <- try_transport a; b <- try_transport b; Some (a, b)%core
+           | _ => None
+           end%expr_pat%expr%option.
+      Definition invert_Literal {t} (e : expr t)
+        : option (type.interp base.interp t)
+        := match e with
+           | expr.Ident _ idc => ident.invert_Literal idc
+           | _ => None
+           end%expr_pat%expr.
+      Definition invert_nil {t} (e : expr (base.type.list t)) : bool
+        := match invert_Ident e with
+           | Some (ident.nil _) => true
+           | _ => false
+           end.
+      Local Notation if_arrow2 f t
+        := (match t return Type with
+            | (a -> b -> c)%etype => f a b c
+            | _ => unit
+            end) (only parsing).
+      Definition invert_cons {t} (e : expr (base.type.list t))
+        : option (expr t * expr (base.type.list t))
+        := match invert_AppIdent2 e with
+           | Some (existT _ (idc, x, y))
+             => match idc in ident.ident t
+                      return if_arrow2 (fun a b c => expr a) t
+                             -> if_arrow2 (fun a b c => expr b) t
+                             -> option match t return Type with
+                                       | (a -> b -> type.base (base.type.list t))
+                                         => (expr t * expr (base.type.list t))%type
+                                       | _ => unit
+                                       end%etype
+                with
+                | ident.cons t => fun x xs => Some (x, xs)
+                | _ => fun _ _ => None
+                end x y
+           | _ => None
+           end.
+    End with_var.
+
+    Fixpoint reflect_list_cps' {var t} (e : @expr.expr base.type ident var t) {struct e}
+      : ~> option (list (@expr.expr base.type ident var (type.base match t return base.type with
+                                                                   | type.base (base.type.list t) => t
+                                                                   | _ => base.type.unit
+                                                                   end)))
+      := match e in expr.expr t return ~> option (list (@expr.expr base.type ident var (type.base match t return base.type with
+                                                                                                  | type.base (base.type.list t) => t
+                                                                                                  | _ => base.type.unit
+                                                                                                  end)))
+         with
+         | [] => (return (Some nil))
+         | x :: xs
+           => (x' <-- type.try_transport_cps base.try_make_transport_cps (@expr.expr base.type ident var) _ _ x;
+                xs' <-- @reflect_list_cps' var _ xs;
+                xs' <-- type.try_transport_cps base.try_make_transport_cps (fun t => list (@expr.expr _ _ _ (type.base match t return base.type with
+                                                                                                                  | type.base (base.type.list t) => t
+                                                                                                                  | _ => base.type.unit
+                                                                                                                  end))) _ _ xs';
+              return (Some (x' :: xs')%list))
+         | _ => (return None)
+         end%expr_pat%expr%cps.
+
+    Definition reflect_list_cps {var t} (e : @expr.expr base.type ident var (type.base (base.type.list t)))
+      : ~> option (list (@expr.expr base.type ident var (type.base t)))
+      := reflect_list_cps' e.
+    Global Arguments reflect_list_cps {var t} e [T] k.
+
+    Definition reflect_list {var t} (e : @expr.expr base.type ident var (type.base (base.type.list t)))
+      : option (list (@expr.expr base.type ident var (type.base t)))
+      := reflect_list_cps e id.
+  End invert_expr.
+
+  Module DefaultValue.
+    (** This module provides "default" inhabitants for the
+        interpretation of PHOAS types and for the PHOAS [expr] type.
+        These values are used for things like [nth_default] and in
+        other places where we need to provide a dummy value in cases
+        that will never actually be reached in correctly used code. *)
+    Module type.
+      Module base.
+        Fixpoint default {t : base.type} : base.interp t
+          := match t with
+             | base.type.unit => tt
+             | base.type.Z => (-1)%Z
+             | base.type.nat => 0%nat
+             | base.type.bool => true
+             | base.type.list _ => nil
+             | base.type.prod A B
+               => (@default A, @default B)
+             end.
+      End base.
+      Fixpoint default {t} : type.interp base.interp t
+        := match t with
+           | type.base x => @base.default x
+           | type.arrow s d => fun _ => @default d
+           end.
+    End type.
+
+    Module expr.
+      Module base.
+        Section with_var.
+          Context {var : type.type base.type -> Type}.
+          Fixpoint default {t : base.type} : @expr base.type ident var (type.base t)
+            := match t with
+               | base.type.prod A B
+                 => (@default A, @default B)
+               | base.type.list A => #ident.nil
+               | base.type.unit as t
+               | base.type.Z as t
+               | base.type.nat as t
+               | base.type.bool as t
+                 => ##(@type.base.default t)
+               end%expr.
+        End with_var.
+
+        Definition Default {t : base.type} : expr.Expr (type.base t) := fun _ => default.
+      End base.
+
+      Section with_var.
+        Context {var : type base.type -> Type}.
+        Fixpoint default {t : type base.type} : @expr base.type ident var t
+          := match t with
+             | type.base x => base.default
+             | type.arrow s d => λ _, @default d
+             end%expr.
+      End with_var.
+
+      Definition Default {t} : expr.Expr t := fun _ => default.
+    End expr.
+  End DefaultValue.
+
+  Module Import defaults.
+    Notation expr := (@expr base.type ident).
+    Notation Expr := (@expr.Expr base.type ident).
+    Notation type := (type base.type).
+    Global Coercion type_base (t : base.type) : type := type.base t.
+    Global Arguments type_base _ / .
+    Notation interp := (@expr.interp base.type ident base.interp (@ident.interp)).
+    Notation Interp := (@expr.Interp base.type ident base.interp (@ident.interp)).
+    Ltac reify_type ty := type.reify ltac:(base.reify) base.type ty.
+    Notation reify_type t := (ltac:(let rt := reify_type t in exact rt)) (only parsing).
+    Notation reify_type_of e := (reify_type ((fun t (_ : t) => t) _ e)) (only parsing).
+  End defaults.
+
+  Notation reify_list := ident.reify_list.
+
+  Module GallinaReify.
+    Module base.
+      Section reify.
+        Context {var : type -> Type}.
+        Fixpoint reify {t : base.type} {struct t}
+          : base.interp t -> @expr var t
+          := match t return base.interp t -> expr t with
+             | base.type.prod A B as t
+               => fun '((a, b) : base.interp A * base.interp B)
+                  => (@reify A a, @reify B b)%expr
+             | base.type.list A as t
+               => fun x : list (base.interp A)
+                  => reify_list (List.map (@reify A) x)
+             | base.type.unit as t
+             | base.type.Z as t
+             | base.type.bool as t
+             | base.type.nat as t
+               => fun x : base.interp t
+                  => (##x)%expr
+             end.
+      End reify.
+
+      Definition Reify_as (t : base.type) (v : base.interp t) : Expr t
+        := fun var => reify v.
+
+      (** [Reify] does Ltac type inference to get the type *)
+      Notation Reify v
+        := (Reify_as (base.reify_type_of v) (fun _ => v)) (only parsing).
+    End base.
+
+    Section value.
+      Context (var : type -> Type).
+      Fixpoint value (t : type)
+        := match t return Type with
+           | type.arrow s d => var s -> value d
+           | type.base t => base.interp t
+           end%type.
+    End value.
+
+    Section reify.
+      Context {var : type -> Type}.
+      Fixpoint reify {t : type} {struct t}
+        : value var t -> @expr var t
+        := match t return value var t -> expr t with
+           | type.arrow s d
+             => fun (f : var s -> value var d)
+                => (λ x , @reify d (f x))%expr
+           | type.base t
+             => @base.reify var t
+           end.
+    End reify.
+
+    Fixpoint reify_as_interp {t : type} {struct t}
+      : type.interp base.interp t -> @expr (type.interp base.interp) t
+      := match t return type.interp base.interp t -> expr t with
+         | type.arrow s d
+           => fun (f : type.interp base.interp s -> type.interp base.interp d)
+              => (λ x , @reify_as_interp d (f x))%expr
+         | type.base t
+           => @base.reify _ t
+         end.
+
+    Definition Reify_as (t : type) (v : forall var, value var t) : Expr t
+      := fun var => reify (v _).
+
+    (** [Reify] does Ltac type inference to get the type *)
+    Notation Reify v
+      := (Reify_as (reify_type_of v) (fun _ => v)) (only parsing).
+  End GallinaReify.
+
+  Module GeneralizeVar.
+    (** In both lazy and cbv evaluation strategies, reduction under
+        lambdas is only done at the very end.  This means that if we
+        have a computation which returns a PHOAS syntax tree, and we
+        plug in two different values for [var], the computation is run
+        twice.  This module provides a way of computing a
+        representation of terms which does not suffer from this issue.
+        By computing a flat representation, and then going back to
+        PHOAS, the cbv strategy will fully compute the preceeding
+        PHOAS passes only once, and the lazy strategy will share
+        computation among the various uses of [var] (because there are
+        no lambdas to get blocked on) and thus will also compute the
+        preceeding PHOAS passes only once. *)
+    Module Flat.
+      Inductive expr : type -> Set :=
+      | Ident {t} (idc : ident t) : expr t
+      | Var (t : type) (n : positive) : expr t
+      | Abs (s : type) (n : positive) {d} (f : expr d) : expr (s -> d)
+      | App {s d} (f : expr (s -> d)) (x : expr s) : expr d
+      | LetIn {A B} (n : positive) (ex : expr A) (eC : expr B) : expr B.
+    End Flat.
+
+    Definition ERROR {T} (v : T) : T. exact v. Qed.
+
+    Fixpoint to_flat' {t} (e : @expr (fun _ => PositiveMap.key) t)
+             (cur_idx : PositiveMap.key)
+      : Flat.expr t
+      := match e in expr.expr t return Flat.expr t with
+         | expr.Var t v => Flat.Var t v
+         | expr.App s d f x => Flat.App
+                                 (@to_flat' _ f cur_idx)
+                                 (@to_flat' _ x cur_idx)
+         | expr.Ident t idc => Flat.Ident idc
+         | expr.Abs s d f
+           => Flat.Abs s cur_idx
+                       (@to_flat'
+                          d (f cur_idx)
+                          (Pos.succ cur_idx))
+         | expr.LetIn A B ex eC
+           => Flat.LetIn
+                cur_idx
+                (@to_flat' A ex cur_idx)
+                (@to_flat'
+                   B (eC cur_idx)
+                   (Pos.succ cur_idx))
+         end.
+
+    Fixpoint from_flat {t} (e : Flat.expr t)
+      : forall var, PositiveMap.t { t : type & var t } -> @expr var t
+      := match e in Flat.expr t return forall var, _ -> expr t with
+         | Flat.Var t v
+           => fun var ctx
+              => match (tv <- PositiveMap.find v ctx;
+                          type.try_transport base.try_make_transport_cps var _ _ (projT2 tv))%option with
+                 | Some v => expr.Var v
+                 | None => ERROR DefaultValue.expr.default
+                 end
+         | Flat.Ident t idc => fun var ctx => expr.Ident idc
+         | Flat.App s d f x
+           => let f' := @from_flat _ f in
+              let x' := @from_flat _ x in
+              fun var ctx => expr.App (f' var ctx) (x' var ctx)
+         | Flat.Abs s cur_idx d f
+           => let f' := @from_flat d f in
+              fun var ctx
+              => expr.Abs (fun v => f' var (PositiveMap.add cur_idx (existT _ s v) ctx))
+         | Flat.LetIn A B cur_idx ex eC
+           => let ex' := @from_flat A ex in
+              let eC' := @from_flat B eC in
+              fun var ctx
+              => expr.LetIn
+                   (ex' var ctx)
+                   (fun v => eC' var (PositiveMap.add cur_idx (existT _ A v) ctx))
+         end.
+
+    Definition to_flat {t} (e : expr t) : Flat.expr t
+      := to_flat' e 1%positive.
+    Definition ToFlat {t} (E : Expr t) : Flat.expr t
+      := to_flat (E _).
+    Definition FromFlat {t} (e : Flat.expr t) : Expr t
+      := let e' := @from_flat t e in
+         fun var => e' var (PositiveMap.empty _).
+    Definition GeneralizeVar {t} (e : @expr (fun _ => PositiveMap.key) t) : Expr t
+      := FromFlat (to_flat e).
+  End GeneralizeVar.
+End Compilers.
+Global Opaque Compilers.ident.cast. (* This should never be unfolded except in [LanguageWf] *)