move src/Experiments/NewPipeline/ to src/

1 files changed, 2496 insertions, 0 deletions

diff --git a/src/GENERATEDIdentifiersWithoutTypes.v b/src/GENERATEDIdentifiersWithoutTypes.v
new file mode 100644
index 000000000..a682df8a2
--- /dev/null
+++ b/src/GENERATEDIdentifiersWithoutTypes.v
@@ -0,0 +1,2496 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.FSets.FMapPositive.
+Require Import Coq.MSets.MSetPositive.
+Require Import Coq.Lists.List.
+Require Import Crypto.Util.CPSNotations.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.PrimitiveSigma.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Language.
+Import ListNotations. Local Open Scope list_scope.
+Import PrimitiveSigma.Primitive.
+
+Module Compilers.
+  Set Boolean Equality Schemes.
+  Set Decidable Equality Schemes.
+  Export Language.Compilers.
+
+  Local Notation type_of_list := (fold_right (fun A B => prod A B) unit).
+  Local Notation type_of_list_cps := (fold_right (fun a K => a -> K)).
+  Module pattern.
+    Notation EvarMap := (PositiveMap.t Compilers.base.type).
+    Module base.
+      Local Notation einterp := type.interp.
+      Module type.
+        Inductive type := var (p : positive) | type_base (t : Compilers.base.type.base) | prod (A B : type) | list (A : type).
+      End type.
+      Notation type := type.type.
+
+      Fixpoint relax (t : Compilers.base.type) : type
+        := match t with
+           | Compilers.base.type.type_base t => type.type_base t
+           | Compilers.base.type.prod A B => type.prod (relax A) (relax B)
+           | Compilers.base.type.list A => type.list (relax A)
+           end.
+
+      Fixpoint subst_default (ptype : type) (evar_map : EvarMap) : Compilers.base.type
+        := match ptype with
+           | type.var p => match PositiveMap.find p evar_map with
+                           | Some t => t
+                           | None => Compilers.base.type.type_base base.type.unit
+                           end
+           | type.type_base t => Compilers.base.type.type_base t
+           | type.prod A B
+             => Compilers.base.type.prod (subst_default A evar_map) (subst_default B evar_map)
+           | type.list A => Compilers.base.type.list (subst_default A evar_map)
+           end.
+
+      Fixpoint collect_vars (t : type) : PositiveSet.t
+        := match t with
+           | type.var p => PositiveSet.add p PositiveSet.empty
+           | type.type_base t => PositiveSet.empty
+           | type.prod A B => PositiveSet.union (collect_vars A) (collect_vars B)
+           | type.list A => collect_vars A
+           end.
+
+      Module Notations.
+        Global Coercion type.type_base : Compilers.base.type.base >-> type.type.
+        Bind Scope pbtype_scope with type.type.
+        (*Bind Scope ptype_scope with Compilers.type.type type.type.*) (* COQBUG(https://github.com/coq/coq/issues/7699) *)
+        Delimit Scope ptype_scope with ptype.
+        Delimit Scope pbtype_scope with pbtype.
+        Notation "A * B" := (type.prod A%ptype B%ptype) : ptype_scope.
+        Notation "A * B" := (type.prod A%pbtype B%pbtype) : pbtype_scope.
+        Notation "()" := (type.type_base base.type.unit) : pbtype_scope.
+        Notation "()" := (type.base (type.type_base base.type.unit)) : ptype_scope.
+        Notation "A -> B" := (type.arrow A%ptype B%ptype) : ptype_scope.
+        Notation "' n" := (type.var n) : pbtype_scope.
+        Notation "' n" := (type.base (type.var n)) : ptype_scope.
+        Notation "'1" := (type.var 1) : pbtype_scope.
+        Notation "'2" := (type.var 2) : pbtype_scope.
+        Notation "'3" := (type.var 3) : pbtype_scope.
+        Notation "'4" := (type.var 4) : pbtype_scope.
+        Notation "'5" := (type.var 5) : pbtype_scope.
+        Notation "'1" := (type.base (type.var 1)) : ptype_scope.
+        Notation "'2" := (type.base (type.var 2)) : ptype_scope.
+        Notation "'3" := (type.base (type.var 3)) : ptype_scope.
+        Notation "'4" := (type.base (type.var 4)) : ptype_scope.
+        Notation "'5" := (type.base (type.var 5)) : ptype_scope.
+      End Notations.
+    End base.
+    Notation type := (type.type base.type).
+    Export base.Notations.
+
+    Module type.
+      Fixpoint relax (t : type.type Compilers.base.type) : type
+        := match t with
+           | type.base t => type.base (base.relax t)
+           | type.arrow s d => type.arrow (relax s) (relax d)
+           end.
+
+      Fixpoint subst_default (ptype : type) (evar_map : EvarMap) : type.type Compilers.base.type
+        := match ptype with
+           | type.base t => type.base (base.subst_default t evar_map)
+           | type.arrow A B => type.arrow (subst_default A evar_map) (subst_default B evar_map)
+           end.
+
+      Fixpoint collect_vars (t : type) : PositiveSet.t
+        := match t with
+           | type.base t => base.collect_vars t
+           | type.arrow s d => PositiveSet.union (collect_vars s) (collect_vars d)
+           end.
+    End type.
+
+    (*
+    Set Printing Coercions.
+    Redirect "/tmp/pr" Print Compilers.ident.ident.
+    Redirect "/tmp/sm" Show Match Compilers.ident.ident.
+    *)
+    (*
+<<<
+#!/usr/bin/env python2
+import re, os
+
+print_ident = r"""Inductive ident : defaults.type -> Set :=
+    Literal : forall t : base.type.base,
+              base.interp (Compilers.base.type.type_base t) ->
+              ident
+                ((fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base t))
+  | Nat_succ : ident
+                 ((fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.nat) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.nat))%ptype
+  | Nat_pred : ident
+                 ((fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.nat) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.nat))%ptype
+  | Nat_max : ident
+                ((fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.nat) ->
+                 (fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.nat) ->
+                 (fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.nat))%ptype
+  | Nat_mul : ident
+                ((fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.nat) ->
+                 (fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.nat) ->
+                 (fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.nat))%ptype
+  | Nat_add : ident
+                ((fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.nat) ->
+                 (fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.nat) ->
+                 (fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.nat))%ptype
+  | Nat_sub : ident
+                ((fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.nat) ->
+                 (fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.nat) ->
+                 (fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.nat))%ptype
+  | nil : forall t : Compilers.base.type,
+          ident
+            ((fun x : Compilers.base.type => type.base x)
+               (Compilers.base.type.list t))
+  | cons : forall t : Compilers.base.type,
+           ident
+             ((fun x : Compilers.base.type => type.base x) t ->
+              (fun x : Compilers.base.type => type.base x)
+                (Compilers.base.type.list t) ->
+              (fun x : Compilers.base.type => type.base x)
+                (Compilers.base.type.list t))%ptype
+  | pair : forall A B : Compilers.base.type,
+           ident
+             ((fun x : Compilers.base.type => type.base x) A ->
+              (fun x : Compilers.base.type => type.base x) B ->
+              (fun x : Compilers.base.type => type.base x) (A * B)%etype)%ptype
+  | fst : forall A B : Compilers.base.type,
+          ident
+            ((fun x : Compilers.base.type => type.base x) (A * B)%etype ->
+             (fun x : Compilers.base.type => type.base x) A)%ptype
+  | snd : forall A B : Compilers.base.type,
+          ident
+            ((fun x : Compilers.base.type => type.base x) (A * B)%etype ->
+             (fun x : Compilers.base.type => type.base x) B)%ptype
+  | prod_rect : forall A B T : Compilers.base.type,
+                ident
+                  (((fun x : Compilers.base.type => type.base x) A ->
+                    (fun x : Compilers.base.type => type.base x) B ->
+                    (fun x : Compilers.base.type => type.base x) T) ->
+                   (fun x : Compilers.base.type => type.base x) (A * B)%etype ->
+                   (fun x : Compilers.base.type => type.base x) T)%ptype
+  | bool_rect : forall T : Compilers.base.type,
+                ident
+                  (((fun x : Compilers.base.type => type.base x) ()%etype ->
+                    (fun x : Compilers.base.type => type.base x) T) ->
+                   ((fun x : Compilers.base.type => type.base x) ()%etype ->
+                    (fun x : Compilers.base.type => type.base x) T) ->
+                   (fun x : Compilers.base.type => type.base x)
+                     (Compilers.base.type.type_base base.type.bool) ->
+                   (fun x : Compilers.base.type => type.base x) T)%ptype
+  | nat_rect : forall P : Compilers.base.type,
+               ident
+                 (((fun x : Compilers.base.type => type.base x) ()%etype ->
+                   (fun x : Compilers.base.type => type.base x) P) ->
+                  ((fun x : Compilers.base.type => type.base x)
+                     (Compilers.base.type.type_base base.type.nat) ->
+                   (fun x : Compilers.base.type => type.base x) P ->
+                   (fun x : Compilers.base.type => type.base x) P) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.nat) ->
+                  (fun x : Compilers.base.type => type.base x) P)%ptype
+  | nat_rect_arrow : forall P Q : Compilers.base.type,
+                     ident
+                       (((fun x : Compilers.base.type => type.base x) P ->
+                         (fun x : Compilers.base.type => type.base x) Q) ->
+                        ((fun x : Compilers.base.type => type.base x)
+                           (Compilers.base.type.type_base base.type.nat) ->
+                         ((fun x : Compilers.base.type => type.base x) P ->
+                          (fun x : Compilers.base.type => type.base x) Q) ->
+                         (fun x : Compilers.base.type => type.base x) P ->
+                         (fun x : Compilers.base.type => type.base x) Q) ->
+                        (fun x : Compilers.base.type => type.base x)
+                          (Compilers.base.type.type_base base.type.nat) ->
+                        (fun x : Compilers.base.type => type.base x) P ->
+                        (fun x : Compilers.base.type => type.base x) Q)%ptype
+  | list_rect : forall A P : Compilers.base.type,
+                ident
+                  (((fun x : Compilers.base.type => type.base x) ()%etype ->
+                    (fun x : Compilers.base.type => type.base x) P) ->
+                   ((fun x : Compilers.base.type => type.base x) A ->
+                    (fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.list A) ->
+                    (fun x : Compilers.base.type => type.base x) P ->
+                    (fun x : Compilers.base.type => type.base x) P) ->
+                   (fun x : Compilers.base.type => type.base x)
+                     (Compilers.base.type.list A) ->
+                   (fun x : Compilers.base.type => type.base x) P)%ptype
+  | list_case : forall A P : Compilers.base.type,
+                ident
+                  (((fun x : Compilers.base.type => type.base x) ()%etype ->
+                    (fun x : Compilers.base.type => type.base x) P) ->
+                   ((fun x : Compilers.base.type => type.base x) A ->
+                    (fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.list A) ->
+                    (fun x : Compilers.base.type => type.base x) P) ->
+                   (fun x : Compilers.base.type => type.base x)
+                     (Compilers.base.type.list A) ->
+                   (fun x : Compilers.base.type => type.base x) P)%ptype
+  | List_length : forall T : Compilers.base.type,
+                  ident
+                    ((fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.list T) ->
+                     (fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.nat))%ptype
+  | List_seq : ident
+                 ((fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.nat) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.nat) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.list
+                       (Compilers.base.type.type_base base.type.nat)))%ptype
+  | List_firstn : forall A : Compilers.base.type,
+                  ident
+                    ((fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.nat) ->
+                     (fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.list A) ->
+                     (fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.list A))%ptype
+  | List_skipn : forall A : Compilers.base.type,
+                 ident
+                   ((fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.type_base base.type.nat) ->
+                    (fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.list A) ->
+                    (fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.list A))%ptype
+  | List_repeat : forall A : Compilers.base.type,
+                  ident
+                    ((fun x : Compilers.base.type => type.base x) A ->
+                     (fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.nat) ->
+                     (fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.list A))%ptype
+  | List_combine : forall A B : Compilers.base.type,
+                   ident
+                     ((fun x : Compilers.base.type => type.base x)
+                        (Compilers.base.type.list A) ->
+                      (fun x : Compilers.base.type => type.base x)
+                        (Compilers.base.type.list B) ->
+                      (fun x : Compilers.base.type => type.base x)
+                        (Compilers.base.type.list (A * B)))%ptype
+  | List_map : forall A B : Compilers.base.type,
+               ident
+                 (((fun x : Compilers.base.type => type.base x) A ->
+                   (fun x : Compilers.base.type => type.base x) B) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.list A) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.list B))%ptype
+  | List_app : forall A : Compilers.base.type,
+               ident
+                 ((fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.list A) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.list A) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.list A))%ptype
+  | List_rev : forall A : Compilers.base.type,
+               ident
+                 ((fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.list A) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.list A))%ptype
+  | List_flat_map : forall A B : Compilers.base.type,
+                    ident
+                      (((fun x : Compilers.base.type => type.base x) A ->
+                        (fun x : Compilers.base.type => type.base x)
+                          (Compilers.base.type.list B)) ->
+                       (fun x : Compilers.base.type => type.base x)
+                         (Compilers.base.type.list A) ->
+                       (fun x : Compilers.base.type => type.base x)
+                         (Compilers.base.type.list B))%ptype
+  | List_partition : forall A : Compilers.base.type,
+                     ident
+                       (((fun x : Compilers.base.type => type.base x) A ->
+                         (fun x : Compilers.base.type => type.base x)
+                           (Compilers.base.type.type_base base.type.bool)) ->
+                        (fun x : Compilers.base.type => type.base x)
+                          (Compilers.base.type.list A) ->
+                        (fun x : Compilers.base.type => type.base x)
+                          (Compilers.base.type.list A *
+                           Compilers.base.type.list A)%etype)%ptype
+  | List_fold_right : forall A B : Compilers.base.type,
+                      ident
+                        (((fun x : Compilers.base.type => type.base x) B ->
+                          (fun x : Compilers.base.type => type.base x) A ->
+                          (fun x : Compilers.base.type => type.base x) A) ->
+                         (fun x : Compilers.base.type => type.base x) A ->
+                         (fun x : Compilers.base.type => type.base x)
+                           (Compilers.base.type.list B) ->
+                         (fun x : Compilers.base.type => type.base x) A)%ptype
+  | List_update_nth : forall T : Compilers.base.type,
+                      ident
+                        ((fun x : Compilers.base.type => type.base x)
+                           (Compilers.base.type.type_base base.type.nat) ->
+                         ((fun x : Compilers.base.type => type.base x) T ->
+                          (fun x : Compilers.base.type => type.base x) T) ->
+                         (fun x : Compilers.base.type => type.base x)
+                           (Compilers.base.type.list T) ->
+                         (fun x : Compilers.base.type => type.base x)
+                           (Compilers.base.type.list T))%ptype
+  | List_nth_default : forall T : Compilers.base.type,
+                       ident
+                         ((fun x : Compilers.base.type => type.base x) T ->
+                          (fun x : Compilers.base.type => type.base x)
+                            (Compilers.base.type.list T) ->
+                          (fun x : Compilers.base.type => type.base x)
+                            (Compilers.base.type.type_base base.type.nat) ->
+                          (fun x : Compilers.base.type => type.base x) T)%ptype
+  | Z_add : ident
+              ((fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_mul : ident
+              ((fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_pow : ident
+              ((fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_sub : ident
+              ((fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_opp : ident
+              ((fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_div : ident
+              ((fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_modulo : ident
+                 ((fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.Z) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.Z) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_log2 : ident
+               ((fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z) ->
+                (fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_log2_up : ident
+                  ((fun x : Compilers.base.type => type.base x)
+                     (Compilers.base.type.type_base base.type.Z) ->
+                   (fun x : Compilers.base.type => type.base x)
+                     (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_eqb : ident
+              ((fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.bool))%ptype
+  | Z_leb : ident
+              ((fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.bool))%ptype
+  | Z_geb : ident
+              ((fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.bool))%ptype
+  | Z_of_nat : ident
+                 ((fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.nat) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_to_nat : ident
+                 ((fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.Z) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.nat))%ptype
+  | Z_shiftr : ident
+                 ((fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.Z) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.Z) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_shiftl : ident
+                 ((fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.Z) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.Z) ->
+                  (fun x : Compilers.base.type => type.base x)
+                    (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_land : ident
+               ((fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z) ->
+                (fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z) ->
+                (fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_lor : ident
+              ((fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z) ->
+               (fun x : Compilers.base.type => type.base x)
+                 (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_bneg : ident
+               ((fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z) ->
+                (fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_lnot_modulo : ident
+                      ((fun x : Compilers.base.type => type.base x)
+                         (Compilers.base.type.type_base base.type.Z) ->
+                       (fun x : Compilers.base.type => type.base x)
+                         (Compilers.base.type.type_base base.type.Z) ->
+                       (fun x : Compilers.base.type => type.base x)
+                         (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_mul_split : ident
+                    ((fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.Z) ->
+                     (fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.Z) ->
+                     (fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.Z) ->
+                     (fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.Z *
+                        Compilers.base.type.type_base base.type.Z)%etype)%ptype
+  | Z_add_get_carry : ident
+                        ((fun x : Compilers.base.type => type.base x)
+                           (Compilers.base.type.type_base base.type.Z) ->
+                         (fun x : Compilers.base.type => type.base x)
+                           (Compilers.base.type.type_base base.type.Z) ->
+                         (fun x : Compilers.base.type => type.base x)
+                           (Compilers.base.type.type_base base.type.Z) ->
+                         (fun x : Compilers.base.type => type.base x)
+                           (Compilers.base.type.type_base base.type.Z *
+                            Compilers.base.type.type_base base.type.Z)%etype)%ptype
+  | Z_add_with_carry : ident
+                         ((fun x : Compilers.base.type => type.base x)
+                            (Compilers.base.type.type_base base.type.Z) ->
+                          (fun x : Compilers.base.type => type.base x)
+                            (Compilers.base.type.type_base base.type.Z) ->
+                          (fun x : Compilers.base.type => type.base x)
+                            (Compilers.base.type.type_base base.type.Z) ->
+                          (fun x : Compilers.base.type => type.base x)
+                            (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_add_with_get_carry : ident
+                             ((fun x : Compilers.base.type => type.base x)
+                                (Compilers.base.type.type_base base.type.Z) ->
+                              (fun x : Compilers.base.type => type.base x)
+                                (Compilers.base.type.type_base base.type.Z) ->
+                              (fun x : Compilers.base.type => type.base x)
+                                (Compilers.base.type.type_base base.type.Z) ->
+                              (fun x : Compilers.base.type => type.base x)
+                                (Compilers.base.type.type_base base.type.Z) ->
+                              (fun x : Compilers.base.type => type.base x)
+                                (Compilers.base.type.type_base base.type.Z *
+                                 Compilers.base.type.type_base base.type.Z)%etype)%ptype
+  | Z_sub_get_borrow : ident
+                         ((fun x : Compilers.base.type => type.base x)
+                            (Compilers.base.type.type_base base.type.Z) ->
+                          (fun x : Compilers.base.type => type.base x)
+                            (Compilers.base.type.type_base base.type.Z) ->
+                          (fun x : Compilers.base.type => type.base x)
+                            (Compilers.base.type.type_base base.type.Z) ->
+                          (fun x : Compilers.base.type => type.base x)
+                            (Compilers.base.type.type_base base.type.Z *
+                             Compilers.base.type.type_base base.type.Z)%etype)%ptype
+  | Z_sub_with_get_borrow : ident
+                              ((fun x : Compilers.base.type => type.base x)
+                                 (Compilers.base.type.type_base base.type.Z) ->
+                               (fun x : Compilers.base.type => type.base x)
+                                 (Compilers.base.type.type_base base.type.Z) ->
+                               (fun x : Compilers.base.type => type.base x)
+                                 (Compilers.base.type.type_base base.type.Z) ->
+                               (fun x : Compilers.base.type => type.base x)
+                                 (Compilers.base.type.type_base base.type.Z) ->
+                               (fun x : Compilers.base.type => type.base x)
+                                 (Compilers.base.type.type_base base.type.Z *
+                                  Compilers.base.type.type_base base.type.Z)%etype)%ptype
+  | Z_zselect : ident
+                  ((fun x : Compilers.base.type => type.base x)
+                     (Compilers.base.type.type_base base.type.Z) ->
+                   (fun x : Compilers.base.type => type.base x)
+                     (Compilers.base.type.type_base base.type.Z) ->
+                   (fun x : Compilers.base.type => type.base x)
+                     (Compilers.base.type.type_base base.type.Z) ->
+                   (fun x : Compilers.base.type => type.base x)
+                     (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_add_modulo : ident
+                     ((fun x : Compilers.base.type => type.base x)
+                        (Compilers.base.type.type_base base.type.Z) ->
+                      (fun x : Compilers.base.type => type.base x)
+                        (Compilers.base.type.type_base base.type.Z) ->
+                      (fun x : Compilers.base.type => type.base x)
+                        (Compilers.base.type.type_base base.type.Z) ->
+                      (fun x : Compilers.base.type => type.base x)
+                        (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_rshi : ident
+               ((fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z) ->
+                (fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z) ->
+                (fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z) ->
+                (fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z) ->
+                (fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_cc_m : ident
+               ((fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z) ->
+                (fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z) ->
+                (fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_cast : zrange ->
+             ident
+               ((fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z) ->
+                (fun x : Compilers.base.type => type.base x)
+                  (Compilers.base.type.type_base base.type.Z))%ptype
+  | Z_cast2 : zrange * zrange ->
+              ident
+                ((fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.Z *
+                    Compilers.base.type.type_base base.type.Z)%etype ->
+                 (fun x : Compilers.base.type => type.base x)
+                   (Compilers.base.type.type_base base.type.Z *
+                    Compilers.base.type.type_base base.type.Z)%etype)%ptype
+  | fancy_add : Z ->
+                Z ->
+                ident
+                  ((fun x : Compilers.base.type => type.base x)
+                     (Compilers.base.type.type_base base.type.Z *
+                      Compilers.base.type.type_base base.type.Z)%etype ->
+                   (fun x : Compilers.base.type => type.base x)
+                     (Compilers.base.type.type_base base.type.Z *
+                      Compilers.base.type.type_base base.type.Z)%etype)%ptype
+  | fancy_addc : Z ->
+                 Z ->
+                 ident
+                   ((fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.type_base base.type.Z *
+                       Compilers.base.type.type_base base.type.Z *
+                       Compilers.base.type.type_base base.type.Z)%etype ->
+                    (fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.type_base base.type.Z *
+                       Compilers.base.type.type_base base.type.Z)%etype)%ptype
+  | fancy_sub : Z ->
+                Z ->
+                ident
+                  ((fun x : Compilers.base.type => type.base x)
+                     (Compilers.base.type.type_base base.type.Z *
+                      Compilers.base.type.type_base base.type.Z)%etype ->
+                   (fun x : Compilers.base.type => type.base x)
+                     (Compilers.base.type.type_base base.type.Z *
+                      Compilers.base.type.type_base base.type.Z)%etype)%ptype
+  | fancy_subb : Z ->
+                 Z ->
+                 ident
+                   ((fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.type_base base.type.Z *
+                       Compilers.base.type.type_base base.type.Z *
+                       Compilers.base.type.type_base base.type.Z)%etype ->
+                    (fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.type_base base.type.Z *
+                       Compilers.base.type.type_base base.type.Z)%etype)%ptype
+  | fancy_mulll : Z ->
+                  ident
+                    ((fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.Z *
+                        Compilers.base.type.type_base base.type.Z)%etype ->
+                     (fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.Z))%ptype
+  | fancy_mullh : Z ->
+                  ident
+                    ((fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.Z *
+                        Compilers.base.type.type_base base.type.Z)%etype ->
+                     (fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.Z))%ptype
+  | fancy_mulhl : Z ->
+                  ident
+                    ((fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.Z *
+                        Compilers.base.type.type_base base.type.Z)%etype ->
+                     (fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.Z))%ptype
+  | fancy_mulhh : Z ->
+                  ident
+                    ((fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.Z *
+                        Compilers.base.type.type_base base.type.Z)%etype ->
+                     (fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.Z))%ptype
+  | fancy_rshi : Z ->
+                 Z ->
+                 ident
+                   ((fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.type_base base.type.Z *
+                       Compilers.base.type.type_base base.type.Z)%etype ->
+                    (fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.type_base base.type.Z))%ptype
+  | fancy_selc : ident
+                   ((fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.type_base base.type.Z *
+                       Compilers.base.type.type_base base.type.Z *
+                       Compilers.base.type.type_base base.type.Z)%etype ->
+                    (fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.type_base base.type.Z))%ptype
+  | fancy_selm : Z ->
+                 ident
+                   ((fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.type_base base.type.Z *
+                       Compilers.base.type.type_base base.type.Z *
+                       Compilers.base.type.type_base base.type.Z)%etype ->
+                    (fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.type_base base.type.Z))%ptype
+  | fancy_sell : ident
+                   ((fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.type_base base.type.Z *
+                       Compilers.base.type.type_base base.type.Z *
+                       Compilers.base.type.type_base base.type.Z)%etype ->
+                    (fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.type_base base.type.Z))%ptype
+  | fancy_addm : ident
+                   ((fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.type_base base.type.Z *
+                       Compilers.base.type.type_base base.type.Z *
+                       Compilers.base.type.type_base base.type.Z)%etype ->
+                    (fun x : Compilers.base.type => type.base x)
+                      (Compilers.base.type.type_base base.type.Z))%ptype
+
+"""
+show_match_ident = r"""match # with
+ | ident.Literal t v =>
+ | ident.Nat_succ =>
+ | ident.Nat_pred =>
+ | ident.Nat_max =>
+ | ident.Nat_mul =>
+ | ident.Nat_add =>
+ | ident.Nat_sub =>
+ | ident.nil t =>
+ | ident.cons t =>
+ | ident.pair A B =>
+ | ident.fst A B =>
+ | ident.snd A B =>
+ | ident.prod_rect A B T =>
+ | ident.bool_rect T =>
+ | ident.nat_rect P =>
+ | ident.nat_rect_arrow P Q =>
+ | ident.list_rect A P =>
+ | ident.list_case A P =>
+ | ident.List_length T =>
+ | ident.List_seq =>
+ | ident.List_firstn A =>
+ | ident.List_skipn A =>
+ | ident.List_repeat A =>
+ | ident.List_combine A B =>
+ | ident.List_map A B =>
+ | ident.List_app A =>
+ | ident.List_rev A =>
+ | ident.List_flat_map A B =>
+ | ident.List_partition A =>
+ | ident.List_fold_right A B =>
+ | ident.List_update_nth T =>
+ | ident.List_nth_default T =>
+ | ident.Z_add =>
+ | ident.Z_mul =>
+ | ident.Z_pow =>
+ | ident.Z_sub =>
+ | ident.Z_opp =>
+ | ident.Z_div =>
+ | ident.Z_modulo =>
+ | ident.Z_log2 =>
+ | ident.Z_log2_up =>
+ | ident.Z_eqb =>
+ | ident.Z_leb =>
+ | ident.Z_geb =>
+ | ident.Z_of_nat =>
+ | ident.Z_to_nat =>
+ | ident.Z_shiftr =>
+ | ident.Z_shiftl =>
+ | ident.Z_land =>
+ | ident.Z_lor =>
+ | ident.Z_bneg =>
+ | ident.Z_lnot_modulo =>
+ | ident.Z_mul_split =>
+ | ident.Z_add_get_carry =>
+ | ident.Z_add_with_carry =>
+ | ident.Z_add_with_get_carry =>
+ | ident.Z_sub_get_borrow =>
+ | ident.Z_sub_with_get_borrow =>
+ | ident.Z_zselect =>
+ | ident.Z_add_modulo =>
+ | ident.Z_rshi =>
+ | ident.Z_cc_m =>
+ | ident.Z_cast range =>
+ | ident.Z_cast2 range =>
+ | ident.fancy_add log2wordmax imm =>
+ | ident.fancy_addc log2wordmax imm =>
+ | ident.fancy_sub log2wordmax imm =>
+ | ident.fancy_subb log2wordmax imm =>
+ | ident.fancy_mulll log2wordmax =>
+ | ident.fancy_mullh log2wordmax =>
+ | ident.fancy_mulhl log2wordmax =>
+ | ident.fancy_mulhh log2wordmax =>
+ | ident.fancy_rshi log2wordmax x =>
+ | ident.fancy_selc =>
+ | ident.fancy_selm log2wordmax =>
+ | ident.fancy_sell =>
+ | ident.fancy_addm =>
+ end
+
+"""
+remake = False
+if remake:
+  assert(os.path.exists('/tmp/pr.out'))
+  assert(os.path.exists('/tmp/sm.out'))
+  with open('/tmp/pr.out', 'r') as f: print_ident = re.sub(r'^For.*\n', '', f.read(), flags=re.MULTILINE)
+  with open('/tmp/sm.out', 'r') as f: show_match_ident = f.read()
+
+prefix = 'Compilers.'
+indent0 = '    '
+indent1 = '  ' + indent0
+indent2 = '  ' + indent1
+#exts = ('Unit', 'Z', 'Bool', 'Nat')
+base_types = [('%sbase.type.' % prefix) + i for i in ('unit', 'Z', 'bool', 'nat')]
+type_or_set = 'Type'
+ctors = [i.strip('|=> ').split(' ') for i in show_match_ident.split('\n') if i.strip().startswith('|')]
+assert(ctors[0][0] == 'ident.Literal')
+assert(len(ctors[0]) > 1)
+#ctors = [[ctors[0][0] + ext] + ctors[0][2:] for ext in exts] + ctors[1:]
+ctors_with_prefix = [[prefix + i[0]] + i[1:] for i in ctors]
+ctors_no_prefix = [[i[0].replace('ident.', '')] + i[1:] for i in ctors]
+pctors = [i[0] for i in ctors_no_prefix]
+def get_dep_types(case):
+  dep_tys = re.findall('forall ([^:]+):([^,]+),', case)
+  if len(dep_tys) == 0: return []
+  dep_tys = dep_tys[0]
+  return [dep_tys[-1].strip()] * len([i for i in dep_tys[0].split(' ') if i.strip()])
+split_print_ident = print_ident.replace('  Literal ', ' | Literal ').replace('\n', ' ').split('|')[1:]
+ttypes = [get_dep_types(case) for case in split_print_ident]
+ctypes = [[i.strip() for i in re.sub(r'forall [^,]+,', '', i[i.find(':')+1:i.find('ident')]).strip(' ->').split('->') if i.strip()]
+          for i in split_print_ident]
+crettypes = [prefix + 'ident.' + re.sub(r'\(fun x : [^ ]+ => ([^ ]+) x\)', r'\1', re.sub('  +', ' ', i[i.find('ident'):])).strip()
+             for i in split_print_ident]
+named_ttypes_with_prefix = [[(name, ty) for name, ty in zip(ctor[1:], tys)]
+                            for ctor, tys in zip(ctors, ttypes)]
+named_ttypes = [[(name, ty.replace(prefix, '')) for name, ty in nt] for nt in named_ttypes_with_prefix]
+pctors_with_typed_args = [(pctor + ' ' + ' '.join('{%s : %s}' % name_ty for name_ty in ntys)).strip()
+                          for pctor, ntys in zip(pctors, named_ttypes)]
+pctors_with_args = [(pctor + ' ' + ' '.join(name for name, ty in ntys)).strip()
+                    for pctor, ntys in zip(pctors, named_ttypes)]
+pctors_with_underscores = [(pctor + ' ' + ' '.join('_' for name, ty in ntys)).strip()
+                           for pctor, ntys in zip(pctors, named_ttypes)]
+rettypes = [i.replace(prefix + 'ident.ident', 'ident').replace(prefix, '').replace('%etype', '%pbtype') for i in crettypes]
+
+# N.B. We assume forall-quantification in the types has names that match the arguments from Show Match
+
+retcode = r"""Require Import Coq.ZArith.ZArith.
+Require Import Coq.FSets.FMapPositive.
+Require Import Coq.MSets.MSetPositive.
+Require Import Coq.Lists.List.
+Require Import Crypto.Util.CPSNotations.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.PrimitiveSigma.
+Require Import Crypto.Util.Notations.
+Require Import Crypto.Language.
+Import ListNotations. Local Open Scope list_scope.
+Import PrimitiveSigma.Primitive.
+
+Module Compilers.
+  Set Boolean Equality Schemes.
+  Set Decidable Equality Schemes.
+  Export Language.Compilers.
+
+  Local Notation type_of_list := (fold_right (fun A B => prod A B) unit).
+  Local Notation type_of_list_cps := (fold_right (fun a K => a -> K)).
+  Module pattern.
+    Notation EvarMap := (PositiveMap.t Compilers.base.type).
+    Module base.
+      Local Notation einterp := type.interp.
+      Module type.
+        Inductive type := var (p : positive) | type_base (t : Compilers.base.type.base) | prod (A B : type) | list (A : type).
+      End type.
+      Notation type := type.type.
+
+      Fixpoint relax (t : Compilers.base.type) : type
+        := match t with
+           | Compilers.base.type.type_base t => type.type_base t
+           | Compilers.base.type.prod A B => type.prod (relax A) (relax B)
+           | Compilers.base.type.list A => type.list (relax A)
+           end.
+
+      Fixpoint subst_default (ptype : type) (evar_map : EvarMap) : Compilers.base.type
+        := match ptype with
+           | type.var p => match PositiveMap.find p evar_map with
+                           | Some t => t
+                           | None => Compilers.base.type.type_base base.type.unit
+                           end
+           | type.type_base t => Compilers.base.type.type_base t
+           | type.prod A B
+             => Compilers.base.type.prod (subst_default A evar_map) (subst_default B evar_map)
+           | type.list A => Compilers.base.type.list (subst_default A evar_map)
+           end.
+
+      Fixpoint collect_vars (t : type) : PositiveSet.t
+        := match t with
+           | type.var p => PositiveSet.add p PositiveSet.empty
+           | type.type_base t => PositiveSet.empty
+           | type.prod A B => PositiveSet.union (collect_vars A) (collect_vars B)
+           | type.list A => collect_vars A
+           end.
+
+      Module Notations.
+        Global Coercion type.type_base : Compilers.base.type.base >-> type.type.
+        Bind Scope pbtype_scope with type.type.
+        (*Bind Scope ptype_scope with Compilers.type.type type.type.*) (* COQBUG(https://github.com/coq/coq/issues/7699) *)
+        Delimit Scope ptype_scope with ptype.
+        Delimit Scope pbtype_scope with pbtype.
+        Notation "A * B" := (type.prod A%ptype B%ptype) : ptype_scope.
+        Notation "A * B" := (type.prod A%pbtype B%pbtype) : pbtype_scope.
+        Notation "()" := (type.type_base base.type.unit) : pbtype_scope.
+        Notation "()" := (type.base (type.type_base base.type.unit)) : ptype_scope.
+        Notation "A -> B" := (type.arrow A%ptype B%ptype) : ptype_scope.
+        Notation "' n" := (type.var n) : pbtype_scope.
+        Notation "' n" := (type.base (type.var n)) : ptype_scope.
+        Notation "'1" := (type.var 1) : pbtype_scope.
+        Notation "'2" := (type.var 2) : pbtype_scope.
+        Notation "'3" := (type.var 3) : pbtype_scope.
+        Notation "'4" := (type.var 4) : pbtype_scope.
+        Notation "'5" := (type.var 5) : pbtype_scope.
+        Notation "'1" := (type.base (type.var 1)) : ptype_scope.
+        Notation "'2" := (type.base (type.var 2)) : ptype_scope.
+        Notation "'3" := (type.base (type.var 3)) : ptype_scope.
+        Notation "'4" := (type.base (type.var 4)) : ptype_scope.
+        Notation "'5" := (type.base (type.var 5)) : ptype_scope.
+      End Notations.
+    End base.
+    Notation type := (type.type base.type).
+    Export base.Notations.
+
+    Module type.
+      Fixpoint relax (t : type.type Compilers.base.type) : type
+        := match t with
+           | type.base t => type.base (base.relax t)
+           | type.arrow s d => type.arrow (relax s) (relax d)
+           end.
+
+      Fixpoint subst_default (ptype : type) (evar_map : EvarMap) : type.type Compilers.base.type
+        := match ptype with
+           | type.base t => type.base (base.subst_default t evar_map)
+           | type.arrow A B => type.arrow (subst_default A evar_map) (subst_default B evar_map)
+           end.
+
+      Fixpoint collect_vars (t : type) : PositiveSet.t
+        := match t with
+           | type.base t => base.collect_vars t
+           | type.arrow s d => PositiveSet.union (collect_vars s) (collect_vars d)
+           end.
+    End type.
+
+    (""" + """*
+    Set Printing Coercions.
+    Redirect "/tmp/pr" Print Compilers.ident.ident.
+    Redirect "/tmp/sm" Show Match Compilers.ident.ident.
+    *""" + """)
+"""
+
+def fold_right_pair(ls, tt='tt'):
+  if len(ls) == 0: return tt
+  return '(' + ls[0] + ', ' + fold_right_pair(ls[1:], tt=tt) + ')'
+
+def addnewline(s): return re.sub(r' +$', '', s + '\n', flags=re.MULTILINE)
+
+def get_updated_contents():
+  contents = open(__file__).read()
+  contents = re.sub(r'^remake = True', r'remake = False', contents, flags=re.MULTILINE)
+  contents = re.sub(r'^print_ident = r""".*?"""', r'print_ident = r"""' + print_ident + r'"""', contents, flags=re.MULTILINE | re.DOTALL)
+  contents = re.sub(r'^show_match_ident = r""".*?"""', r'show_match_ident = r"""' + show_match_ident + r'"""', contents, flags=re.MULTILINE | re.DOTALL)
+  return contents
+
+retcode += addnewline(r"""%s(*
+<<<
+%s
+>>>
+%s*)
+""" % (indent0, get_updated_contents(), indent0))
+
+maxeta = max([len(ttype + ctype) for ttype, ctype in zip(ttypes, ctypes)])
+#if any(len(ttype) > 0 and len(ctype) > 0 for ttype, ctype in zip(ttypes, ctypes)):
+#  retcode += addnewline(r"""%sLocal Notation eta_sigT x := (existT _ (projT1 x) (projT2 x)) (only parsing).""" % indent0)
+if maxeta >= 2:
+  retcode += addnewline(r"""%sLocal Notation eta2 x := (Datatypes.fst x, Datatypes.snd x) (only parsing).""" % indent0)
+  retcode += addnewline(r"""%sLocal Notation eta2r x := (Datatypes.fst x, Datatypes.snd x) (only parsing).""" % indent0)
+for i in range(3, maxeta+1):
+  retcode += addnewline(r"""%sLocal Notation eta%d x := (eta%d (Datatypes.fst x), Datatypes.snd x) (only parsing).""" % (indent0, i, i-1))
+  retcode += addnewline(r"""%sLocal Notation eta%dr x := (Datatypes.fst x, eta%dr (Datatypes.snd x)) (only parsing).""" % (indent0, i, i-1))
+retcode += addnewline('')
+
+def do_adjust_type(ctor, ctype):
+  return len(ctor) > 1 and 'Literal' in ctor[0]
+
+retcode += r"""
+    Module Raw.
+      Module ident.
+"""
+
+retcode += addnewline(r"""%sInductive ident :=
+%s| %s.
+""" % (indent2, indent2, ('\n' + indent2 + '| ').join(pctors)))
+
+def make_prod_of_types(named_ttype, ctype):
+  if len(named_ttype + ctype) == 0: return 'unit'
+  if len(ctype) == 0: return ' * '.join(t for n, t in named_ttype)
+  if len(named_ttype) == 0: return ' * '.join(ctype)
+  if len(named_ttype) == 1: return '{ %s : %s & %s }' % (named_ttype[0][0], named_ttype[0][1], ' * '.join(ctype))
+  return "{ tys : %s & let '(%s) := eta%d tys in %s }" % (' * '.join(t for n, t in named_ttype),
+                                                          ', '.join(n for n, t in named_ttype),
+                                                          len(named_ttype),
+                                                          ' * '.join(ctype))
+
+def make_pair_of_types(named_ttype, ctype, ctor):
+  if len(named_ttype + ctype) == 0: return 'tt'
+  if len(named_ttype + ctype) == 1: return ctor[-1]
+  if len(named_ttype) == 0 or len(ctype) == 0: return '(%s)' % ', '.join(ctor[-len(named_ttype + ctype):])
+  pr1 = (named_ttype[0][0] if len(named_ttype) == 1 else '(%s)' % ', '.join(n for n, t in named_ttype))
+  pr2 = (ctor[-1] if len(ctype) == 1 else '(%s)' % ', '.join(ctor[-len(ctype):]))
+  return '(existT _ %s %s)' % (pr1, pr2)
+
+def make_fun_project(named_ttype, ctype, ctor):
+  if len(named_ttype + ctype) == 0: return 'fun _ => '
+  if len(named_ttype + ctype) == 1: return 'fun ' + ctor[-1] + ' => '
+  if len(named_ttype) == 0 or len(ctype) == 0: return "fun arg => let '(%s) := eta%d arg in " % (', '.join(ctor[-len(named_ttype + ctype):]), len(named_ttype + ctype))
+  pr1 = (named_ttype[0][0] if len(named_ttype) == 1 else '(%s)' % ', '.join(n for n, t in named_ttype))
+  pr2 = (ctor[-1] if len(ctype) == 1 else '(%s)' % ', '.join(ctor[-len(ctype):]))
+  pr1_eta = ('projT1 arg' if len(named_ttype) == 1 else 'eta%d (projT1 arg)' % len(named_ttype))
+  pr2_eta = ('projT2 arg' if len(ctype) == 1 else 'eta%d (projT2 arg)' % len(ctype))
+  return "fun arg => let '(%s, %s) := (%s, %s) in " % (pr1, pr2, pr1_eta, pr2_eta)
+
+def make_fun_project_list(ctype, ctor):
+  if len(ctype) == 0: return 'fun _ => '
+  return "fun arg => let '%s := eta%dr arg in " % (fold_right_pair(ctor[-len(ctype):], tt='_'), len(ctype)+1)
+
+def make_fun_project_match(named_ttype, ctype, ctor, retty, body):
+  if len(named_ttype + ctype) == 0: return 'fun _ => ' + body
+  if len(named_ttype + ctype) == 1: return 'fun ' + ctor[-1] + ' => ' + body
+  if len(named_ttype) == 0 or len(ctype) == 0:
+    return "fun arg => match eta%d arg as arg' return %s with (%s) => %s end" % (len(named_ttype + ctype), retty % "arg'", ', '.join(ctor[-len(named_ttype + ctype):]), body)
+  pr1 = (named_ttype[0][0] if len(named_ttype) == 1 else '(%s)' % ', '.join(n for n, t in named_ttype))
+  pr2 = (ctor[-1] if len(ctype) == 1 else '(%s)' % ', '.join(ctor[-len(ctype):]))
+  pr1_eta = ('projT1 arg' if len(named_ttype) == 1 else 'eta%d (projT1 arg)' % len(named_ttype))
+  pr2_eta = ('projT2 arg' if len(ctype) == 1 else 'eta%d (projT2 arg)' % len(ctype))
+  return "fun arg => match existT _ (%s) (%s) as arg' return %s with existT %s %s => %s end" % (pr1_eta, pr2_eta, retty % "arg'", pr1, pr2, body)
+
+retcode += addnewline((r"""%sDefinition full_types (idc : ident) : %s
+  := match idc return %s with
+     | %s
+     end%%type.
+""" % (indent2, type_or_set, type_or_set,
+       '\n     | '.join(pctor + ' => ' + make_prod_of_types(named_ttype, ctype)
+                        for pctor, named_ttype, ctype in zip(pctors, named_ttypes_with_prefix, ctypes)))).replace('\n', '\n' + indent2))
+
+retcode += addnewline((r"""%sDefinition is_simple (idc : ident) : bool
+  := match idc with
+     | %s
+     end.
+""" % (indent2,
+       '\n     | '.join(pctor + ' => ' + ('true' if len(named_ttype) == 0 else 'false')
+                        for pctor, named_ttype in zip(pctors, named_ttypes_with_prefix)))).replace('\n', '\n' + indent2))
+
+retcode += addnewline((r"""%sDefinition invert_bind_args {t} (idc : %sident.ident t) (pidc : ident) : option (full_types pidc)
+  := match pidc, idc return option (full_types pidc) with
+     | %s
+     | %s
+       => None
+     end%%cps.
+""" % (indent2, prefix,
+       '\n     | '.join(pctor + ', ' + ' '.join(ctor) + ' => Some ' + make_pair_of_types(named_ttype, ctype, ctor)
+                        for pctor, ctor, named_ttype, ctype in zip(pctors, ctors_with_prefix, named_ttypes_with_prefix, ctypes)),
+       '\n     | '.join(pctor + ', _' for pctor in pctors))).replace('\n', '\n' + indent2))
+
+retcode += addnewline((r"""%sDefinition type_of (pidc : ident) : full_types pidc -> %stype %sbase.type
+  := match pidc return full_types pidc -> _ with
+     | %s
+     end%%etype.
+""" % (indent2, prefix, prefix,
+       '\n     | '.join(pctor + ' => '
+                        + make_fun_project(named_ttype, ctype, ctor) + cretty.replace(prefix + 'ident.ident ', '')
+                        for pctor, ctor, named_ttype, ctype, cretty in zip(pctors, ctors_with_prefix, named_ttypes_with_prefix, ctypes, crettypes)))).replace('\n', '\n' + indent2))
+retcode += addnewline((r"""%sDefinition to_typed (pidc : ident) : forall args : full_types pidc, %sident.ident (type_of pidc args)
+  := match pidc return forall args : full_types pidc, %sident.ident (type_of pidc args) with
+     | %s
+     end.
+""" % (indent2, prefix, prefix,
+       '\n     | '.join(pctor + ' => '
+                        + make_fun_project_match(named_ttype, ctype, ctor, '%sident.ident (type_of %s %%s)' % (prefix, pctor), ("@" + ' '.join(ctor)))
+                        for pctor, ctor, named_ttype, ctype in zip(pctors, ctors_with_prefix, named_ttypes_with_prefix, ctypes)))).replace('\n', '\n' + indent2))
+
+retcode += r"""      End ident.
+      Notation ident := ident.ident.
+    End Raw.
+"""
+
+retcode +=r"""
+    Module ident.
+"""
+retcode += addnewline((r"""%sDefinition eta_ident_cps {T : %stype %sbase.type -> Type} {t} (idc : %sident.ident t)
+           (f : forall t', %sident.ident t' -> T t')
+  : T t
+  := match idc with
+     | %s
+     end.
+""" % (indent1, prefix, prefix, prefix, prefix,
+       '\n     | '.join(' '.join(ctor) + ' => f _ '
+                        + (('%s' if len(ctor) == 1 else '(@%s)')
+                           % ' '.join(ctor))
+                        for ctor in ctors_with_prefix))).replace('\n', '\n' + indent1))
+
+retcode += addnewline(r"""%sInductive ident : type -> Set :=
+%s| %s.
+""" % (indent1, indent1, ('\n' + indent1 + '| ').join('%s : %s' % ct for ct in zip(pctors_with_typed_args, rettypes))))
+
+retcode += addnewline((r"""%sDefinition strip_types {t} (idc : ident t) : Raw.ident
+  := match idc with
+     | %s
+     end.
+""" % (indent1, '\n     | '.join('@' + pctor_with_args + ' => Raw.ident.' + pctor for pctor_with_args, pctor in zip(pctors_with_args, pctors)))).replace('\n', '\n' + indent1))
+
+# here we assume that non-dependent arguments do not depend on dependent
+# arguments which become generalized to patterns --- that is, only dependent
+# arguments of type base.type.base can show up in the types of other identifier
+# arguments.
+
+retcode += addnewline((r"""%sDefinition arg_types {t} (idc : ident t) : list %s
+  := match idc return list %s with
+     | %s
+     end%%type.
+""" % (indent1, type_or_set, type_or_set,
+       '\n     | '.join('@' + pctor + ' => [' + '; '.join(i + ' : ' + type_or_set for i in ctype) + ']'
+                        for pctor, ctype in zip(pctors_with_args, ctypes)))).replace('\n', '\n' + indent1))
+
+def to_type_var(name, ty):
+  ty = ty.replace(prefix, '')
+  return ({'base.type.base': 'type.base (base.type.type_base %s)' % name,
+           'base.type': 'type.base %s' % name,
+           'type': name,
+           'type.type base.type': name})[ty]
+
+#retcode += addnewline((r"""%sDefinition type_vars {t} (idc : ident t) : list type
+#  := match idc with
+#     | %s
+#     end%%type.
+#""" % (indent1,
+#       '\n     | '.join('@' + pctor + ' => [' + '; '.join(to_type_var(n, t) for n, t in named_ttype) + ']'
+#                        for pctor, named_ttype in zip(pctors_with_args, named_ttypes)))).replace('\n', '\n' + indent1))
+
+retcode += addnewline((r"""%sDefinition to_typed {t} (idc : ident t) (evm : EvarMap) : type_of_list (arg_types idc) -> %sident.ident (pattern.type.subst_default t evm)
+  := match idc in ident t return type_of_list (arg_types idc) -> %sident.ident (pattern.type.subst_default t evm) with
+     | %s
+     end.
+""" % (indent1, prefix, prefix,
+       '\n     | '.join('@' + pctor + ' => '
+                        + make_fun_project_list(ctype, ctor)
+                        + '@' + ' '.join([ctor[0]] + ['_' for _ in ctor[1:len(ctor)-len(ctype)]] + ctor[len(ctor)-len(ctype):])
+                        for pctor, ctor, ctype in zip(pctors_with_args, ctors_with_prefix, ctypes)))).replace('\n', '\n' + indent1))
+
+assert(ctors[0][0] == 'ident.Literal')
+assert(len(ctypes[0]) == 1)
+
+retcode += addnewline((r"""%sDefinition unify {t t'} (pidc : ident t) (idc : %sident.ident t') : option (type_of_list (@arg_types t pidc))
+  := match pidc, idc return option (type_of_list (arg_types pidc)) with
+     | %s
+     | %s
+     | %s
+       => None
+     end%%cps.
+""" % (indent1, prefix,
+       '\n     | '.join('@' + pctor + ' ' + ty + ', ' + ' '.join([ctor[0], ty] + ctor[2:]) + ' => Some ' + fold_right_pair(ctor[-len(ctype):])
+                        for pctor, ctor, ctype in zip(pctors[:1], ctors_with_prefix[:1], ctypes[:1])
+                        for ty in base_types),
+       '\n     | '.join('@' + pctor + ', ' + ' '.join([ctor[0]] + [i + "'" for i in ctor[1:]]) + ' => Some ' + ('tt' if len(ctype) == 0 else fold_right_pair([i + "'" for i in ctor[-len(ctype):]]))
+                        for pctor, ctor, ctype in zip(pctors_with_args[1:], ctors_with_prefix[1:], ctypes[1:])),
+       '\n     | '.join('@' + pctor + ', _' for pctor, named_ttype in zip(pctors_with_underscores, named_ttypes)))).replace('\n', '\n' + indent1))
+
+def relax_type_var(name, ty):
+  ty = ty.replace(prefix, '')
+  return ({'base.type.base': name,
+           'base.type': '(base.relax %s)' % name,
+           'type': '(type.relax %s)' % name,
+           'type.type base.type': '(type.relax %s)' % name})[ty]
+
+retcode += addnewline((r"""%sDefinition of_typed_ident {t} (idc : %sident.ident t) : ident (type.relax t)
+  := match idc with
+     | %s
+     end.
+""" % (indent1, prefix, '\n     | '.join(' '.join(ctor) + ' => @' + pctor + ' ' + ' '.join(relax_type_var(n, t) for n, t in named_ttype) for ctor, pctor, named_ttype in zip(ctors_with_prefix, pctors, named_ttypes)))).replace('\n', '\n' + indent1))
+#
+#
+#retcode += addnewline((r"""%sDefinition retype_ident {t} (idc : %sident.ident t) : match arg_types (of_typed_ident idc) return %s with Some t => t | None => unit end -> %sident.ident t
+#  := match idc in %sident.ident t return match arg_types (of_typed_ident idc) return %s with Some t => t | None => unit end -> %sident.ident t with
+#     | %s
+#     end.
+#""" % (indent1, prefix, type_or_set, prefix, prefix, type_or_set, prefix,
+#       '\n     | '.join(' '.join(ctor) + ' => '
+#                        + ('' if not do_adjust_type(ctor, ctype) else '(')
+#                        + 'fun ' + ('_ => ' if len(ctype) == 0 else ((ctor[-1] + ' => ') if len(ctype) == 1 else "arg => let '(%s) := eta%d arg in " % (', '.join(ctor[-len(ctype):]), len(ctype)))) + "@" + ' '.join(ctor)
+#                        + ('' if not do_adjust_type(ctor, ctype) else
+#                           (') : '
+#                            + ('match arg_types (of_typed_ident %s) return %s with Some t => t | None => unit end -> _'
+#                               % (('%s' if ' ' not in ' '.join(ctor) else '(@%s)') % ' '.join(ctor),
+#                                  type_or_set))
+#                            + ' (* COQBUG(https://github.com/coq/coq/issues/7726) *)'))
+#                        for ctor, ctype in zip(ctors_with_prefix, ctypes)))).replace('\n', '\n' + indent1))
+
+
+
+
+#retcode += addnewline((r"""%sDefinition try_make_transport_ident_cps (P : ident -> Type) (idc1 idc2 : ident) : ~> option (P idc1 -> P idc2)
+#  := match idc1, idc2 with
+#     | %s
+#       => fun T k => k (Some (fun v => v))
+#     | %s
+#       => fun T k => k None
+#     end%%cps.
+#""" % (indent2,
+#       '\n     | '.join(pctor + ', ' + pctor for pctor in pctors),
+#       '\n     | '.join(pctor + ', _' for pctor in pctors))).replace('\n', '\n' + indent2))
+#retcode += addnewline((r"""%sDefinition eta_all_option_cps {T} (f : ident -> option T)
+#  : option (ident -> T)
+#  := (%s;
+#      Some (fun c
+#            => match c with
+#               | %s
+#               end))%%option.
+#""" % (indent2,
+#       ';\n      '.join('f' + pctor + ' <- f ' + ctor[0] for ctor, pctor in zip(ctors_no_prefix, pctors)),
+#       '\n               | '.join(ctor[0] + ' => f' + pctor for pctor, ctor in zip(pctors, ctors_no_prefix)))).replace('\n', '\n' + indent2))
+#retcode += addnewline((r"""%sDefinition orb (f : ident -> bool) : bool
+#  := (%s)%%bool.
+#""" % (indent2, ' || '.join('f ' + pctor for pctor in pctors))).replace('\n', '\n' + indent2))
+
+#retcode += addnewline((r"""%sDefinition bind_args {t} (idc : %sident.ident t) : type_of_list (arg_types (of_typed_ident idc))
+#  := match idc return type_of_list (arg_types (of_typed_ident idc)) with
+#     | %s
+#     end%%cps.
+#""" % (indent1, prefix,
+#       '\n     | '.join(' '.join(ctor) + ' => ' + ('tt' if len(ttype + ctype) == 0 else fold_right_pair(ctor[-len(ttype + ctype):]))
+#                        for ctor, ttype, ctype in zip(ctors_with_prefix, ttypes, ctypes)))).replace('\n', '\n' + indent1))
+#maxeta = max([1+len(ttype + ctype) for ttype, ctype in zip(ttypes, ctypes)])
+#if maxeta >= 2:
+#  retcode += addnewline(r"""%sLocal Notation eta2r x := (Datatypes.fst x, Datatypes.snd x) (only parsing).""" % indent1)
+#for i in range(3, maxeta+1):
+#  retcode += addnewline(r"""%sLocal Notation eta%dr x := (Datatypes.fst x, eta%dr (Datatypes.snd x)) (only parsing).""" % (indent1, i, i-1))
+#retcode += addnewline('')
+#
+#def do_adjust_type(ctor, ctype):
+#  return len(ctor) > 1 and 'Literal' in ctor[0]
+#
+#retcode += addnewline((r"""%sDefinition type_of (pidc : ident) : type_of_list (arg_types pidc) -> %stype %sbase.type
+#  := match pidc return type_of_list (arg_types pidc) -> _ with
+#     | %s
+#     end%%etype.
+#""" % (indent1, prefix, prefix,
+#       '\n     | '.join(pctor + ' => '
+#                        + 'fun ' + ('_ => ' if len(ttype + ctype) == 0 else "arg => let '%s := eta%dr arg in " % (fold_right_pair(ctor[-len(ttype + ctype):], tt='_'), 1+len(ttype + ctype))) + cretty.replace(prefix + 'ident.ident ', '')
+#                        for pctor, ctor, ttype, ctype, cretty in zip(pctors, ctors_with_prefix, ttypes, ctypes, crettypes)))).replace('\n', '\n' + indent1))
+#retcode += addnewline((r"""%sDefinition to_typed (pidc : ident) : forall args : type_of_list (arg_types pidc), %sident.ident (type_of pidc args)
+#  := match pidc return forall args : type_of_list (arg_types pidc), %sident.ident (type_of pidc args) with
+#     | %s
+#     end.
+#""" % (indent1, prefix, prefix,
+#       '\n     | '.join(pctor + ' => '
+#                        + 'fun ' + (('_ => %s' if len(ttype + ctype) == 0 else "arg => match eta%dr arg as args' return %sident.ident (type_of %s args') with %s => %%s end" % (1+len(ttype + ctype), prefix, pctor, fold_right_pair(ctor[-len(ttype + ctype):], tt='_'))) % ("@" + ' '.join(ctor)))
+#                        for pctor, ctor, ttype, ctype in zip(pctors, ctors_with_prefix, ttypes, ctypes)))).replace('\n', '\n' + indent1))
+
+
+
+
+
+retcode += r"""    End ident.
+"""
+
+retcode += addnewline(indent0 + '\n' + indent0 + '(*===*)')
+retcode += r"""
+  End pattern.
+End Compilers.
+"""
+with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
+  f.write(retcode)
+
+>>>
+    *)
+
+    Local Notation eta2 x := (Datatypes.fst x, Datatypes.snd x) (only parsing).
+    Local Notation eta2r x := (Datatypes.fst x, Datatypes.snd x) (only parsing).
+    Local Notation eta3 x := (eta2 (Datatypes.fst x), Datatypes.snd x) (only parsing).
+    Local Notation eta3r x := (Datatypes.fst x, eta2r (Datatypes.snd x)) (only parsing).
+
+
+    Module Raw.
+      Module ident.
+        Inductive ident :=
+        | Literal
+        | Nat_succ
+        | Nat_pred
+        | Nat_max
+        | Nat_mul
+        | Nat_add
+        | Nat_sub
+        | nil
+        | cons
+        | pair
+        | fst
+        | snd
+        | prod_rect
+        | bool_rect
+        | nat_rect
+        | nat_rect_arrow
+        | list_rect
+        | list_case
+        | List_length
+        | List_seq
+        | List_firstn
+        | List_skipn
+        | List_repeat
+        | List_combine
+        | List_map
+        | List_app
+        | List_rev
+        | List_flat_map
+        | List_partition
+        | List_fold_right
+        | List_update_nth
+        | List_nth_default
+        | Z_add
+        | Z_mul
+        | Z_pow
+        | Z_sub
+        | Z_opp
+        | Z_div
+        | Z_modulo
+        | Z_log2
+        | Z_log2_up
+        | Z_eqb
+        | Z_leb
+        | Z_geb
+        | Z_of_nat
+        | Z_to_nat
+        | Z_shiftr
+        | Z_shiftl
+        | Z_land
+        | Z_lor
+        | Z_bneg
+        | Z_lnot_modulo
+        | Z_mul_split
+        | Z_add_get_carry
+        | Z_add_with_carry
+        | Z_add_with_get_carry
+        | Z_sub_get_borrow
+        | Z_sub_with_get_borrow
+        | Z_zselect
+        | Z_add_modulo
+        | Z_rshi
+        | Z_cc_m
+        | Z_cast
+        | Z_cast2
+        | fancy_add
+        | fancy_addc
+        | fancy_sub
+        | fancy_subb
+        | fancy_mulll
+        | fancy_mullh
+        | fancy_mulhl
+        | fancy_mulhh
+        | fancy_rshi
+        | fancy_selc
+        | fancy_selm
+        | fancy_sell
+        | fancy_addm.
+
+        Definition full_types (idc : ident) : Type
+          := match idc return Type with
+             | Literal => { t : base.type.base & base.interp (Compilers.base.type.type_base t) }
+             | Nat_succ => unit
+             | Nat_pred => unit
+             | Nat_max => unit
+             | Nat_mul => unit
+             | Nat_add => unit
+             | Nat_sub => unit
+             | nil => Compilers.base.type
+             | cons => Compilers.base.type
+             | pair => Compilers.base.type * Compilers.base.type
+             | fst => Compilers.base.type * Compilers.base.type
+             | snd => Compilers.base.type * Compilers.base.type
+             | prod_rect => Compilers.base.type * Compilers.base.type * Compilers.base.type
+             | bool_rect => Compilers.base.type
+             | nat_rect => Compilers.base.type
+             | nat_rect_arrow => Compilers.base.type * Compilers.base.type
+             | list_rect => Compilers.base.type * Compilers.base.type
+             | list_case => Compilers.base.type * Compilers.base.type
+             | List_length => Compilers.base.type
+             | List_seq => unit
+             | List_firstn => Compilers.base.type
+             | List_skipn => Compilers.base.type
+             | List_repeat => Compilers.base.type
+             | List_combine => Compilers.base.type * Compilers.base.type
+             | List_map => Compilers.base.type * Compilers.base.type
+             | List_app => Compilers.base.type
+             | List_rev => Compilers.base.type
+             | List_flat_map => Compilers.base.type * Compilers.base.type
+             | List_partition => Compilers.base.type
+             | List_fold_right => Compilers.base.type * Compilers.base.type
+             | List_update_nth => Compilers.base.type
+             | List_nth_default => Compilers.base.type
+             | Z_add => unit
+             | Z_mul => unit
+             | Z_pow => unit
+             | Z_sub => unit
+             | Z_opp => unit
+             | Z_div => unit
+             | Z_modulo => unit
+             | Z_log2 => unit
+             | Z_log2_up => unit
+             | Z_eqb => unit
+             | Z_leb => unit
+             | Z_geb => unit
+             | Z_of_nat => unit
+             | Z_to_nat => unit
+             | Z_shiftr => unit
+             | Z_shiftl => unit
+             | Z_land => unit
+             | Z_lor => unit
+             | Z_bneg => unit
+             | Z_lnot_modulo => unit
+             | Z_mul_split => unit
+             | Z_add_get_carry => unit
+             | Z_add_with_carry => unit
+             | Z_add_with_get_carry => unit
+             | Z_sub_get_borrow => unit
+             | Z_sub_with_get_borrow => unit
+             | Z_zselect => unit
+             | Z_add_modulo => unit
+             | Z_rshi => unit
+             | Z_cc_m => unit
+             | Z_cast => zrange
+             | Z_cast2 => zrange * zrange
+             | fancy_add => Z * Z
+             | fancy_addc => Z * Z
+             | fancy_sub => Z * Z
+             | fancy_subb => Z * Z
+             | fancy_mulll => Z
+             | fancy_mullh => Z
+             | fancy_mulhl => Z
+             | fancy_mulhh => Z
+             | fancy_rshi => Z * Z
+             | fancy_selc => unit
+             | fancy_selm => Z
+             | fancy_sell => unit
+             | fancy_addm => unit
+             end%type.
+
+        Definition is_simple (idc : ident) : bool
+          := match idc with
+             | Literal => false
+             | Nat_succ => true
+             | Nat_pred => true
+             | Nat_max => true
+             | Nat_mul => true
+             | Nat_add => true
+             | Nat_sub => true
+             | nil => false
+             | cons => false
+             | pair => false
+             | fst => false
+             | snd => false
+             | prod_rect => false
+             | bool_rect => false
+             | nat_rect => false
+             | nat_rect_arrow => false
+             | list_rect => false
+             | list_case => false
+             | List_length => false
+             | List_seq => true
+             | List_firstn => false
+             | List_skipn => false
+             | List_repeat => false
+             | List_combine => false
+             | List_map => false
+             | List_app => false
+             | List_rev => false
+             | List_flat_map => false
+             | List_partition => false
+             | List_fold_right => false
+             | List_update_nth => false
+             | List_nth_default => false
+             | Z_add => true
+             | Z_mul => true
+             | Z_pow => true
+             | Z_sub => true
+             | Z_opp => true
+             | Z_div => true
+             | Z_modulo => true
+             | Z_log2 => true
+             | Z_log2_up => true
+             | Z_eqb => true
+             | Z_leb => true
+             | Z_geb => true
+             | Z_of_nat => true
+             | Z_to_nat => true
+             | Z_shiftr => true
+             | Z_shiftl => true
+             | Z_land => true
+             | Z_lor => true
+             | Z_bneg => true
+             | Z_lnot_modulo => true
+             | Z_mul_split => true
+             | Z_add_get_carry => true
+             | Z_add_with_carry => true
+             | Z_add_with_get_carry => true
+             | Z_sub_get_borrow => true
+             | Z_sub_with_get_borrow => true
+             | Z_zselect => true
+             | Z_add_modulo => true
+             | Z_rshi => true
+             | Z_cc_m => true
+             | Z_cast => true
+             | Z_cast2 => true
+             | fancy_add => true
+             | fancy_addc => true
+             | fancy_sub => true
+             | fancy_subb => true
+             | fancy_mulll => true
+             | fancy_mullh => true
+             | fancy_mulhl => true
+             | fancy_mulhh => true
+             | fancy_rshi => true
+             | fancy_selc => true
+             | fancy_selm => true
+             | fancy_sell => true
+             | fancy_addm => true
+             end.
+
+        Definition invert_bind_args {t} (idc : Compilers.ident.ident t) (pidc : ident) : option (full_types pidc)
+          := match pidc, idc return option (full_types pidc) with
+             | Literal, Compilers.ident.Literal t v => Some (existT _ t v)
+             | Nat_succ, Compilers.ident.Nat_succ => Some tt
+             | Nat_pred, Compilers.ident.Nat_pred => Some tt
+             | Nat_max, Compilers.ident.Nat_max => Some tt
+             | Nat_mul, Compilers.ident.Nat_mul => Some tt
+             | Nat_add, Compilers.ident.Nat_add => Some tt
+             | Nat_sub, Compilers.ident.Nat_sub => Some tt
+             | nil, Compilers.ident.nil t => Some t
+             | cons, Compilers.ident.cons t => Some t
+             | pair, Compilers.ident.pair A B => Some (A, B)
+             | fst, Compilers.ident.fst A B => Some (A, B)
+             | snd, Compilers.ident.snd A B => Some (A, B)
+             | prod_rect, Compilers.ident.prod_rect A B T => Some (A, B, T)
+             | bool_rect, Compilers.ident.bool_rect T => Some T
+             | nat_rect, Compilers.ident.nat_rect P => Some P
+             | nat_rect_arrow, Compilers.ident.nat_rect_arrow P Q => Some (P, Q)
+             | list_rect, Compilers.ident.list_rect A P => Some (A, P)
+             | list_case, Compilers.ident.list_case A P => Some (A, P)
+             | List_length, Compilers.ident.List_length T => Some T
+             | List_seq, Compilers.ident.List_seq => Some tt
+             | List_firstn, Compilers.ident.List_firstn A => Some A
+             | List_skipn, Compilers.ident.List_skipn A => Some A
+             | List_repeat, Compilers.ident.List_repeat A => Some A
+             | List_combine, Compilers.ident.List_combine A B => Some (A, B)
+             | List_map, Compilers.ident.List_map A B => Some (A, B)
+             | List_app, Compilers.ident.List_app A => Some A
+             | List_rev, Compilers.ident.List_rev A => Some A
+             | List_flat_map, Compilers.ident.List_flat_map A B => Some (A, B)
+             | List_partition, Compilers.ident.List_partition A => Some A
+             | List_fold_right, Compilers.ident.List_fold_right A B => Some (A, B)
+             | List_update_nth, Compilers.ident.List_update_nth T => Some T
+             | List_nth_default, Compilers.ident.List_nth_default T => Some T
+             | Z_add, Compilers.ident.Z_add => Some tt
+             | Z_mul, Compilers.ident.Z_mul => Some tt
+             | Z_pow, Compilers.ident.Z_pow => Some tt
+             | Z_sub, Compilers.ident.Z_sub => Some tt
+             | Z_opp, Compilers.ident.Z_opp => Some tt
+             | Z_div, Compilers.ident.Z_div => Some tt
+             | Z_modulo, Compilers.ident.Z_modulo => Some tt
+             | Z_log2, Compilers.ident.Z_log2 => Some tt
+             | Z_log2_up, Compilers.ident.Z_log2_up => Some tt
+             | Z_eqb, Compilers.ident.Z_eqb => Some tt
+             | Z_leb, Compilers.ident.Z_leb => Some tt
+             | Z_geb, Compilers.ident.Z_geb => Some tt
+             | Z_of_nat, Compilers.ident.Z_of_nat => Some tt
+             | Z_to_nat, Compilers.ident.Z_to_nat => Some tt
+             | Z_shiftr, Compilers.ident.Z_shiftr => Some tt
+             | Z_shiftl, Compilers.ident.Z_shiftl => Some tt
+             | Z_land, Compilers.ident.Z_land => Some tt
+             | Z_lor, Compilers.ident.Z_lor => Some tt
+             | Z_bneg, Compilers.ident.Z_bneg => Some tt
+             | Z_lnot_modulo, Compilers.ident.Z_lnot_modulo => Some tt
+             | Z_mul_split, Compilers.ident.Z_mul_split => Some tt
+             | Z_add_get_carry, Compilers.ident.Z_add_get_carry => Some tt
+             | Z_add_with_carry, Compilers.ident.Z_add_with_carry => Some tt
+             | Z_add_with_get_carry, Compilers.ident.Z_add_with_get_carry => Some tt
+             | Z_sub_get_borrow, Compilers.ident.Z_sub_get_borrow => Some tt
+             | Z_sub_with_get_borrow, Compilers.ident.Z_sub_with_get_borrow => Some tt
+             | Z_zselect, Compilers.ident.Z_zselect => Some tt
+             | Z_add_modulo, Compilers.ident.Z_add_modulo => Some tt
+             | Z_rshi, Compilers.ident.Z_rshi => Some tt
+             | Z_cc_m, Compilers.ident.Z_cc_m => Some tt
+             | Z_cast, Compilers.ident.Z_cast range => Some range
+             | Z_cast2, Compilers.ident.Z_cast2 range => Some range
+             | fancy_add, Compilers.ident.fancy_add log2wordmax imm => Some (log2wordmax, imm)
+             | fancy_addc, Compilers.ident.fancy_addc log2wordmax imm => Some (log2wordmax, imm)
+             | fancy_sub, Compilers.ident.fancy_sub log2wordmax imm => Some (log2wordmax, imm)
+             | fancy_subb, Compilers.ident.fancy_subb log2wordmax imm => Some (log2wordmax, imm)
+             | fancy_mulll, Compilers.ident.fancy_mulll log2wordmax => Some log2wordmax
+             | fancy_mullh, Compilers.ident.fancy_mullh log2wordmax => Some log2wordmax
+             | fancy_mulhl, Compilers.ident.fancy_mulhl log2wordmax => Some log2wordmax
+             | fancy_mulhh, Compilers.ident.fancy_mulhh log2wordmax => Some log2wordmax
+             | fancy_rshi, Compilers.ident.fancy_rshi log2wordmax x => Some (log2wordmax, x)
+             | fancy_selc, Compilers.ident.fancy_selc => Some tt
+             | fancy_selm, Compilers.ident.fancy_selm log2wordmax => Some log2wordmax
+             | fancy_sell, Compilers.ident.fancy_sell => Some tt
+             | fancy_addm, Compilers.ident.fancy_addm => Some tt
+             | Literal, _
+             | Nat_succ, _
+             | Nat_pred, _
+             | Nat_max, _
+             | Nat_mul, _
+             | Nat_add, _
+             | Nat_sub, _
+             | nil, _
+             | cons, _
+             | pair, _
+             | fst, _
+             | snd, _
+             | prod_rect, _
+             | bool_rect, _
+             | nat_rect, _
+             | nat_rect_arrow, _
+             | list_rect, _
+             | list_case, _
+             | List_length, _
+             | List_seq, _
+             | List_firstn, _
+             | List_skipn, _
+             | List_repeat, _
+             | List_combine, _
+             | List_map, _
+             | List_app, _
+             | List_rev, _
+             | List_flat_map, _
+             | List_partition, _
+             | List_fold_right, _
+             | List_update_nth, _
+             | List_nth_default, _
+             | Z_add, _
+             | Z_mul, _
+             | Z_pow, _
+             | Z_sub, _
+             | Z_opp, _
+             | Z_div, _
+             | Z_modulo, _
+             | Z_log2, _
+             | Z_log2_up, _
+             | Z_eqb, _
+             | Z_leb, _
+             | Z_geb, _
+             | Z_of_nat, _
+             | Z_to_nat, _
+             | Z_shiftr, _
+             | Z_shiftl, _
+             | Z_land, _
+             | Z_lor, _
+             | Z_bneg, _
+             | Z_lnot_modulo, _
+             | Z_mul_split, _
+             | Z_add_get_carry, _
+             | Z_add_with_carry, _
+             | Z_add_with_get_carry, _
+             | Z_sub_get_borrow, _
+             | Z_sub_with_get_borrow, _
+             | Z_zselect, _
+             | Z_add_modulo, _
+             | Z_rshi, _
+             | Z_cc_m, _
+             | Z_cast, _
+             | Z_cast2, _
+             | fancy_add, _
+             | fancy_addc, _
+             | fancy_sub, _
+             | fancy_subb, _
+             | fancy_mulll, _
+             | fancy_mullh, _
+             | fancy_mulhl, _
+             | fancy_mulhh, _
+             | fancy_rshi, _
+             | fancy_selc, _
+             | fancy_selm, _
+             | fancy_sell, _
+             | fancy_addm, _
+               => None
+             end%cps.
+
+        Definition type_of (pidc : ident) : full_types pidc -> Compilers.type Compilers.base.type
+          := match pidc return full_types pidc -> _ with
+             | Literal => fun arg => let '(t, v) := (projT1 arg, projT2 arg) in (type.base (Compilers.base.type.type_base t))
+             | Nat_succ => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
+             | Nat_pred => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
+             | Nat_max => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
+             | Nat_mul => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
+             | Nat_add => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
+             | Nat_sub => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
+             | nil => fun t => (type.base (Compilers.base.type.list t))
+             | cons => fun t => (type.base t -> type.base (Compilers.base.type.list t) -> type.base (Compilers.base.type.list t))%ptype
+             | pair => fun arg => let '(A, B) := eta2 arg in (type.base A -> type.base B -> type.base (A * B)%etype)%ptype
+             | fst => fun arg => let '(A, B) := eta2 arg in (type.base (A * B)%etype -> type.base A)%ptype
+             | snd => fun arg => let '(A, B) := eta2 arg in (type.base (A * B)%etype -> type.base B)%ptype
+             | prod_rect => fun arg => let '(A, B, T) := eta3 arg in ((type.base A -> type.base B -> type.base T) -> type.base (A * B)%etype -> type.base T)%ptype
+             | bool_rect => fun T => ((type.base ()%etype -> type.base T) -> (type.base ()%etype -> type.base T) -> type.base (Compilers.base.type.type_base base.type.bool) -> type.base T)%ptype
+             | nat_rect => fun P => ((type.base ()%etype -> type.base P) -> (type.base (Compilers.base.type.type_base base.type.nat) -> type.base P -> type.base P) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base P)%ptype
+             | nat_rect_arrow => fun arg => let '(P, Q) := eta2 arg in ((type.base P -> type.base Q) -> (type.base (Compilers.base.type.type_base base.type.nat) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base P -> type.base Q)%ptype
+             | list_rect => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype
+             | list_case => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype
+             | List_length => fun T => (type.base (Compilers.base.type.list T) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
+             | List_seq => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.list (Compilers.base.type.type_base base.type.nat)))%ptype
+             | List_firstn => fun A => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list A))%ptype
+             | List_skipn => fun A => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list A))%ptype
+             | List_repeat => fun A => (type.base A -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.list A))%ptype
+             | List_combine => fun arg => let '(A, B) := eta2 arg in (type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list B) -> type.base (Compilers.base.type.list (A * B)))%ptype
+             | List_map => fun arg => let '(A, B) := eta2 arg in ((type.base A -> type.base B) -> type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list B))%ptype
+             | List_app => fun A => (type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list A))%ptype
+             | List_rev => fun A => (type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list A))%ptype
+             | List_flat_map => fun arg => let '(A, B) := eta2 arg in ((type.base A -> type.base (Compilers.base.type.list B)) -> type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list B))%ptype
+             | List_partition => fun A => ((type.base A -> type.base (Compilers.base.type.type_base base.type.bool)) -> type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list A * Compilers.base.type.list A)%etype)%ptype
+             | List_fold_right => fun arg => let '(A, B) := eta2 arg in ((type.base B -> type.base A -> type.base A) -> type.base A -> type.base (Compilers.base.type.list B) -> type.base A)%ptype
+             | List_update_nth => fun T => (type.base (Compilers.base.type.type_base base.type.nat) -> (type.base T -> type.base T) -> type.base (Compilers.base.type.list T) -> type.base (Compilers.base.type.list T))%ptype
+             | List_nth_default => fun T => (type.base T -> type.base (Compilers.base.type.list T) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base T)%ptype
+             | Z_add => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_mul => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_pow => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_sub => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_opp => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_div => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_modulo => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_log2 => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_log2_up => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_eqb => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.bool))%ptype
+             | Z_leb => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.bool))%ptype
+             | Z_geb => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.bool))%ptype
+             | Z_of_nat => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_to_nat => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
+             | Z_shiftr => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_shiftl => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_land => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_lor => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_bneg => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_lnot_modulo => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_mul_split => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
+             | Z_add_get_carry => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
+             | Z_add_with_carry => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_add_with_get_carry => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
+             | Z_sub_get_borrow => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
+             | Z_sub_with_get_borrow => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
+             | Z_zselect => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_add_modulo => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_rshi => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_cc_m => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_cast => fun range => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | Z_cast2 => fun range => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
+             | fancy_add => fun arg => let '(log2wordmax, imm) := eta2 arg in (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
+             | fancy_addc => fun arg => let '(log2wordmax, imm) := eta2 arg in (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
+             | fancy_sub => fun arg => let '(log2wordmax, imm) := eta2 arg in (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
+             | fancy_subb => fun arg => let '(log2wordmax, imm) := eta2 arg in (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
+             | fancy_mulll => fun log2wordmax => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | fancy_mullh => fun log2wordmax => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | fancy_mulhl => fun log2wordmax => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | fancy_mulhh => fun log2wordmax => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | fancy_rshi => fun arg => let '(log2wordmax, x) := eta2 arg in (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | fancy_selc => fun _ => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | fancy_selm => fun log2wordmax => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | fancy_sell => fun _ => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             | fancy_addm => fun _ => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
+             end%etype.
+
+        Definition to_typed (pidc : ident) : forall args : full_types pidc, Compilers.ident.ident (type_of pidc args)
+          := match pidc return forall args : full_types pidc, Compilers.ident.ident (type_of pidc args) with
+             | Literal => fun arg => match existT _ (projT1 arg) (projT2 arg) as arg' return Compilers.ident.ident (type_of Literal arg') with existT t v => @Compilers.ident.Literal t v end
+             | Nat_succ => fun _ => @Compilers.ident.Nat_succ
+             | Nat_pred => fun _ => @Compilers.ident.Nat_pred
+             | Nat_max => fun _ => @Compilers.ident.Nat_max
+             | Nat_mul => fun _ => @Compilers.ident.Nat_mul
+             | Nat_add => fun _ => @Compilers.ident.Nat_add
+             | Nat_sub => fun _ => @Compilers.ident.Nat_sub
+             | nil => fun t => @Compilers.ident.nil t
+             | cons => fun t => @Compilers.ident.cons t
+             | pair => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of pair arg') with (A, B) => @Compilers.ident.pair A B end
+             | fst => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of fst arg') with (A, B) => @Compilers.ident.fst A B end
+             | snd => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of snd arg') with (A, B) => @Compilers.ident.snd A B end
+             | prod_rect => fun arg => match eta3 arg as arg' return Compilers.ident.ident (type_of prod_rect arg') with (A, B, T) => @Compilers.ident.prod_rect A B T end
+             | bool_rect => fun T => @Compilers.ident.bool_rect T
+             | nat_rect => fun P => @Compilers.ident.nat_rect P
+             | nat_rect_arrow => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of nat_rect_arrow arg') with (P, Q) => @Compilers.ident.nat_rect_arrow P Q end
+             | list_rect => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of list_rect arg') with (A, P) => @Compilers.ident.list_rect A P end
+             | list_case => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of list_case arg') with (A, P) => @Compilers.ident.list_case A P end
+             | List_length => fun T => @Compilers.ident.List_length T
+             | List_seq => fun _ => @Compilers.ident.List_seq
+             | List_firstn => fun A => @Compilers.ident.List_firstn A
+             | List_skipn => fun A => @Compilers.ident.List_skipn A
+             | List_repeat => fun A => @Compilers.ident.List_repeat A
+             | List_combine => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of List_combine arg') with (A, B) => @Compilers.ident.List_combine A B end
+             | List_map => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of List_map arg') with (A, B) => @Compilers.ident.List_map A B end
+             | List_app => fun A => @Compilers.ident.List_app A
+             | List_rev => fun A => @Compilers.ident.List_rev A
+             | List_flat_map => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of List_flat_map arg') with (A, B) => @Compilers.ident.List_flat_map A B end
+             | List_partition => fun A => @Compilers.ident.List_partition A
+             | List_fold_right => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of List_fold_right arg') with (A, B) => @Compilers.ident.List_fold_right A B end
+             | List_update_nth => fun T => @Compilers.ident.List_update_nth T
+             | List_nth_default => fun T => @Compilers.ident.List_nth_default T
+             | Z_add => fun _ => @Compilers.ident.Z_add
+             | Z_mul => fun _ => @Compilers.ident.Z_mul
+             | Z_pow => fun _ => @Compilers.ident.Z_pow
+             | Z_sub => fun _ => @Compilers.ident.Z_sub
+             | Z_opp => fun _ => @Compilers.ident.Z_opp
+             | Z_div => fun _ => @Compilers.ident.Z_div
+             | Z_modulo => fun _ => @Compilers.ident.Z_modulo
+             | Z_log2 => fun _ => @Compilers.ident.Z_log2
+             | Z_log2_up => fun _ => @Compilers.ident.Z_log2_up
+             | Z_eqb => fun _ => @Compilers.ident.Z_eqb
+             | Z_leb => fun _ => @Compilers.ident.Z_leb
+             | Z_geb => fun _ => @Compilers.ident.Z_geb
+             | Z_of_nat => fun _ => @Compilers.ident.Z_of_nat
+             | Z_to_nat => fun _ => @Compilers.ident.Z_to_nat
+             | Z_shiftr => fun _ => @Compilers.ident.Z_shiftr
+             | Z_shiftl => fun _ => @Compilers.ident.Z_shiftl
+             | Z_land => fun _ => @Compilers.ident.Z_land
+             | Z_lor => fun _ => @Compilers.ident.Z_lor
+             | Z_bneg => fun _ => @Compilers.ident.Z_bneg
+             | Z_lnot_modulo => fun _ => @Compilers.ident.Z_lnot_modulo
+             | Z_mul_split => fun _ => @Compilers.ident.Z_mul_split
+             | Z_add_get_carry => fun _ => @Compilers.ident.Z_add_get_carry
+             | Z_add_with_carry => fun _ => @Compilers.ident.Z_add_with_carry
+             | Z_add_with_get_carry => fun _ => @Compilers.ident.Z_add_with_get_carry
+             | Z_sub_get_borrow => fun _ => @Compilers.ident.Z_sub_get_borrow
+             | Z_sub_with_get_borrow => fun _ => @Compilers.ident.Z_sub_with_get_borrow
+             | Z_zselect => fun _ => @Compilers.ident.Z_zselect
+             | Z_add_modulo => fun _ => @Compilers.ident.Z_add_modulo
+             | Z_rshi => fun _ => @Compilers.ident.Z_rshi
+             | Z_cc_m => fun _ => @Compilers.ident.Z_cc_m
+             | Z_cast => fun range => @Compilers.ident.Z_cast range
+             | Z_cast2 => fun range => @Compilers.ident.Z_cast2 range
+             | fancy_add => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of fancy_add arg') with (log2wordmax, imm) => @Compilers.ident.fancy_add log2wordmax imm end
+             | fancy_addc => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of fancy_addc arg') with (log2wordmax, imm) => @Compilers.ident.fancy_addc log2wordmax imm end
+             | fancy_sub => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of fancy_sub arg') with (log2wordmax, imm) => @Compilers.ident.fancy_sub log2wordmax imm end
+             | fancy_subb => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of fancy_subb arg') with (log2wordmax, imm) => @Compilers.ident.fancy_subb log2wordmax imm end
+             | fancy_mulll => fun log2wordmax => @Compilers.ident.fancy_mulll log2wordmax
+             | fancy_mullh => fun log2wordmax => @Compilers.ident.fancy_mullh log2wordmax
+             | fancy_mulhl => fun log2wordmax => @Compilers.ident.fancy_mulhl log2wordmax
+             | fancy_mulhh => fun log2wordmax => @Compilers.ident.fancy_mulhh log2wordmax
+             | fancy_rshi => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of fancy_rshi arg') with (log2wordmax, x) => @Compilers.ident.fancy_rshi log2wordmax x end
+             | fancy_selc => fun _ => @Compilers.ident.fancy_selc
+             | fancy_selm => fun log2wordmax => @Compilers.ident.fancy_selm log2wordmax
+             | fancy_sell => fun _ => @Compilers.ident.fancy_sell
+             | fancy_addm => fun _ => @Compilers.ident.fancy_addm
+             end.
+
+      End ident.
+      Notation ident := ident.ident.
+    End Raw.
+
+    Module ident.
+      Definition eta_ident_cps {T : Compilers.type Compilers.base.type -> Type} {t} (idc : Compilers.ident.ident t)
+                 (f : forall t', Compilers.ident.ident t' -> T t')
+        : T t
+        := match idc with
+           | Compilers.ident.Literal t v => f _ (@Compilers.ident.Literal t v)
+           | Compilers.ident.Nat_succ => f _ Compilers.ident.Nat_succ
+           | Compilers.ident.Nat_pred => f _ Compilers.ident.Nat_pred
+           | Compilers.ident.Nat_max => f _ Compilers.ident.Nat_max
+           | Compilers.ident.Nat_mul => f _ Compilers.ident.Nat_mul
+           | Compilers.ident.Nat_add => f _ Compilers.ident.Nat_add
+           | Compilers.ident.Nat_sub => f _ Compilers.ident.Nat_sub
+           | Compilers.ident.nil t => f _ (@Compilers.ident.nil t)
+           | Compilers.ident.cons t => f _ (@Compilers.ident.cons t)
+           | Compilers.ident.pair A B => f _ (@Compilers.ident.pair A B)
+           | Compilers.ident.fst A B => f _ (@Compilers.ident.fst A B)
+           | Compilers.ident.snd A B => f _ (@Compilers.ident.snd A B)
+           | Compilers.ident.prod_rect A B T => f _ (@Compilers.ident.prod_rect A B T)
+           | Compilers.ident.bool_rect T => f _ (@Compilers.ident.bool_rect T)
+           | Compilers.ident.nat_rect P => f _ (@Compilers.ident.nat_rect P)
+           | Compilers.ident.nat_rect_arrow P Q => f _ (@Compilers.ident.nat_rect_arrow P Q)
+           | Compilers.ident.list_rect A P => f _ (@Compilers.ident.list_rect A P)
+           | Compilers.ident.list_case A P => f _ (@Compilers.ident.list_case A P)
+           | Compilers.ident.List_length T => f _ (@Compilers.ident.List_length T)
+           | Compilers.ident.List_seq => f _ Compilers.ident.List_seq
+           | Compilers.ident.List_firstn A => f _ (@Compilers.ident.List_firstn A)
+           | Compilers.ident.List_skipn A => f _ (@Compilers.ident.List_skipn A)
+           | Compilers.ident.List_repeat A => f _ (@Compilers.ident.List_repeat A)
+           | Compilers.ident.List_combine A B => f _ (@Compilers.ident.List_combine A B)
+           | Compilers.ident.List_map A B => f _ (@Compilers.ident.List_map A B)
+           | Compilers.ident.List_app A => f _ (@Compilers.ident.List_app A)
+           | Compilers.ident.List_rev A => f _ (@Compilers.ident.List_rev A)
+           | Compilers.ident.List_flat_map A B => f _ (@Compilers.ident.List_flat_map A B)
+           | Compilers.ident.List_partition A => f _ (@Compilers.ident.List_partition A)
+           | Compilers.ident.List_fold_right A B => f _ (@Compilers.ident.List_fold_right A B)
+           | Compilers.ident.List_update_nth T => f _ (@Compilers.ident.List_update_nth T)
+           | Compilers.ident.List_nth_default T => f _ (@Compilers.ident.List_nth_default T)
+           | Compilers.ident.Z_add => f _ Compilers.ident.Z_add
+           | Compilers.ident.Z_mul => f _ Compilers.ident.Z_mul
+           | Compilers.ident.Z_pow => f _ Compilers.ident.Z_pow
+           | Compilers.ident.Z_sub => f _ Compilers.ident.Z_sub
+           | Compilers.ident.Z_opp => f _ Compilers.ident.Z_opp
+           | Compilers.ident.Z_div => f _ Compilers.ident.Z_div
+           | Compilers.ident.Z_modulo => f _ Compilers.ident.Z_modulo
+           | Compilers.ident.Z_log2 => f _ Compilers.ident.Z_log2
+           | Compilers.ident.Z_log2_up => f _ Compilers.ident.Z_log2_up
+           | Compilers.ident.Z_eqb => f _ Compilers.ident.Z_eqb
+           | Compilers.ident.Z_leb => f _ Compilers.ident.Z_leb
+           | Compilers.ident.Z_geb => f _ Compilers.ident.Z_geb
+           | Compilers.ident.Z_of_nat => f _ Compilers.ident.Z_of_nat
+           | Compilers.ident.Z_to_nat => f _ Compilers.ident.Z_to_nat
+           | Compilers.ident.Z_shiftr => f _ Compilers.ident.Z_shiftr
+           | Compilers.ident.Z_shiftl => f _ Compilers.ident.Z_shiftl
+           | Compilers.ident.Z_land => f _ Compilers.ident.Z_land
+           | Compilers.ident.Z_lor => f _ Compilers.ident.Z_lor
+           | Compilers.ident.Z_bneg => f _ Compilers.ident.Z_bneg
+           | Compilers.ident.Z_lnot_modulo => f _ Compilers.ident.Z_lnot_modulo
+           | Compilers.ident.Z_mul_split => f _ Compilers.ident.Z_mul_split
+           | Compilers.ident.Z_add_get_carry => f _ Compilers.ident.Z_add_get_carry
+           | Compilers.ident.Z_add_with_carry => f _ Compilers.ident.Z_add_with_carry
+           | Compilers.ident.Z_add_with_get_carry => f _ Compilers.ident.Z_add_with_get_carry
+           | Compilers.ident.Z_sub_get_borrow => f _ Compilers.ident.Z_sub_get_borrow
+           | Compilers.ident.Z_sub_with_get_borrow => f _ Compilers.ident.Z_sub_with_get_borrow
+           | Compilers.ident.Z_zselect => f _ Compilers.ident.Z_zselect
+           | Compilers.ident.Z_add_modulo => f _ Compilers.ident.Z_add_modulo
+           | Compilers.ident.Z_rshi => f _ Compilers.ident.Z_rshi
+           | Compilers.ident.Z_cc_m => f _ Compilers.ident.Z_cc_m
+           | Compilers.ident.Z_cast range => f _ (@Compilers.ident.Z_cast range)
+           | Compilers.ident.Z_cast2 range => f _ (@Compilers.ident.Z_cast2 range)
+           | Compilers.ident.fancy_add log2wordmax imm => f _ (@Compilers.ident.fancy_add log2wordmax imm)
+           | Compilers.ident.fancy_addc log2wordmax imm => f _ (@Compilers.ident.fancy_addc log2wordmax imm)
+           | Compilers.ident.fancy_sub log2wordmax imm => f _ (@Compilers.ident.fancy_sub log2wordmax imm)
+           | Compilers.ident.fancy_subb log2wordmax imm => f _ (@Compilers.ident.fancy_subb log2wordmax imm)
+           | Compilers.ident.fancy_mulll log2wordmax => f _ (@Compilers.ident.fancy_mulll log2wordmax)
+           | Compilers.ident.fancy_mullh log2wordmax => f _ (@Compilers.ident.fancy_mullh log2wordmax)
+           | Compilers.ident.fancy_mulhl log2wordmax => f _ (@Compilers.ident.fancy_mulhl log2wordmax)
+           | Compilers.ident.fancy_mulhh log2wordmax => f _ (@Compilers.ident.fancy_mulhh log2wordmax)
+           | Compilers.ident.fancy_rshi log2wordmax x => f _ (@Compilers.ident.fancy_rshi log2wordmax x)
+           | Compilers.ident.fancy_selc => f _ Compilers.ident.fancy_selc
+           | Compilers.ident.fancy_selm log2wordmax => f _ (@Compilers.ident.fancy_selm log2wordmax)
+           | Compilers.ident.fancy_sell => f _ Compilers.ident.fancy_sell
+           | Compilers.ident.fancy_addm => f _ Compilers.ident.fancy_addm
+           end.
+
+      Inductive ident : type -> Set :=
+      | Literal {t : base.type.base} : ident (type.base (base.type.type_base t))
+      | Nat_succ : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat))%ptype
+      | Nat_pred : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat))%ptype
+      | Nat_max : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat))%ptype
+      | Nat_mul : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat))%ptype
+      | Nat_add : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat))%ptype
+      | Nat_sub : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat))%ptype
+      | nil {t : base.type} : ident (type.base (base.type.list t))
+      | cons {t : base.type} : ident (type.base t -> type.base (base.type.list t) -> type.base (base.type.list t))%ptype
+      | pair {A : base.type} {B : base.type} : ident (type.base A -> type.base B -> type.base (A * B)%pbtype)%ptype
+      | fst {A : base.type} {B : base.type} : ident (type.base (A * B)%pbtype -> type.base A)%ptype
+      | snd {A : base.type} {B : base.type} : ident (type.base (A * B)%pbtype -> type.base B)%ptype
+      | prod_rect {A : base.type} {B : base.type} {T : base.type} : ident ((type.base A -> type.base B -> type.base T) -> type.base (A * B)%pbtype -> type.base T)%ptype
+      | bool_rect {T : base.type} : ident ((type.base ()%pbtype -> type.base T) -> (type.base ()%pbtype -> type.base T) -> type.base (base.type.type_base base.type.bool) -> type.base T)%ptype
+      | nat_rect {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base (base.type.type_base base.type.nat) -> type.base P -> type.base P) -> type.base (base.type.type_base base.type.nat) -> type.base P)%ptype
+      | nat_rect_arrow {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base (base.type.type_base base.type.nat) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.type_base base.type.nat) -> type.base P -> type.base Q)%ptype
+      | list_rect {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P -> type.base P) -> type.base (base.type.list A) -> type.base P)%ptype
+      | list_case {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P) -> type.base (base.type.list A) -> type.base P)%ptype
+      | List_length {T : base.type} : ident (type.base (base.type.list T) -> type.base (base.type.type_base base.type.nat))%ptype
+      | List_seq : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.list (base.type.type_base base.type.nat)))%ptype
+      | List_firstn {A : base.type} : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.list A) -> type.base (base.type.list A))%ptype
+      | List_skipn {A : base.type} : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.list A) -> type.base (base.type.list A))%ptype
+      | List_repeat {A : base.type} : ident (type.base A -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.list A))%ptype
+      | List_combine {A : base.type} {B : base.type} : ident (type.base (base.type.list A) -> type.base (base.type.list B) -> type.base (base.type.list (A * B)))%ptype
+      | List_map {A : base.type} {B : base.type} : ident ((type.base A -> type.base B) -> type.base (base.type.list A) -> type.base (base.type.list B))%ptype
+      | List_app {A : base.type} : ident (type.base (base.type.list A) -> type.base (base.type.list A) -> type.base (base.type.list A))%ptype
+      | List_rev {A : base.type} : ident (type.base (base.type.list A) -> type.base (base.type.list A))%ptype
+      | List_flat_map {A : base.type} {B : base.type} : ident ((type.base A -> type.base (base.type.list B)) -> type.base (base.type.list A) -> type.base (base.type.list B))%ptype
+      | List_partition {A : base.type} : ident ((type.base A -> type.base (base.type.type_base base.type.bool)) -> type.base (base.type.list A) -> type.base (base.type.list A * base.type.list A)%pbtype)%ptype
+      | List_fold_right {A : base.type} {B : base.type} : ident ((type.base B -> type.base A -> type.base A) -> type.base A -> type.base (base.type.list B) -> type.base A)%ptype
+      | List_update_nth {T : base.type} : ident (type.base (base.type.type_base base.type.nat) -> (type.base T -> type.base T) -> type.base (base.type.list T) -> type.base (base.type.list T))%ptype
+      | List_nth_default {T : base.type} : ident (type.base T -> type.base (base.type.list T) -> type.base (base.type.type_base base.type.nat) -> type.base T)%ptype
+      | Z_add : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_mul : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_pow : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_sub : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_opp : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_div : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_modulo : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_log2 : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_log2_up : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_eqb : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.bool))%ptype
+      | Z_leb : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.bool))%ptype
+      | Z_geb : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.bool))%ptype
+      | Z_of_nat : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_to_nat : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.nat))%ptype
+      | Z_shiftr : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_shiftl : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_land : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_lor : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_bneg : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_lnot_modulo : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_mul_split : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
+      | Z_add_get_carry : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
+      | Z_add_with_carry : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_add_with_get_carry : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
+      | Z_sub_get_borrow : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
+      | Z_sub_with_get_borrow : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
+      | Z_zselect : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_add_modulo : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_rshi : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_cc_m : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_cast : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
+      | Z_cast2 : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
+      | fancy_add : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
+      | fancy_addc : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
+      | fancy_sub : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
+      | fancy_subb : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
+      | fancy_mulll : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
+      | fancy_mullh : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
+      | fancy_mulhl : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
+      | fancy_mulhh : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
+      | fancy_rshi : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
+      | fancy_selc : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
+      | fancy_selm : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
+      | fancy_sell : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
+      | fancy_addm : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype.
+
+      Definition strip_types {t} (idc : ident t) : Raw.ident
+        := match idc with
+           | @Literal t => Raw.ident.Literal
+           | @Nat_succ => Raw.ident.Nat_succ
+           | @Nat_pred => Raw.ident.Nat_pred
+           | @Nat_max => Raw.ident.Nat_max
+           | @Nat_mul => Raw.ident.Nat_mul
+           | @Nat_add => Raw.ident.Nat_add
+           | @Nat_sub => Raw.ident.Nat_sub
+           | @nil t => Raw.ident.nil
+           | @cons t => Raw.ident.cons
+           | @pair A B => Raw.ident.pair
+           | @fst A B => Raw.ident.fst
+           | @snd A B => Raw.ident.snd
+           | @prod_rect A B T => Raw.ident.prod_rect
+           | @bool_rect T => Raw.ident.bool_rect
+           | @nat_rect P => Raw.ident.nat_rect
+           | @nat_rect_arrow P Q => Raw.ident.nat_rect_arrow
+           | @list_rect A P => Raw.ident.list_rect
+           | @list_case A P => Raw.ident.list_case
+           | @List_length T => Raw.ident.List_length
+           | @List_seq => Raw.ident.List_seq
+           | @List_firstn A => Raw.ident.List_firstn
+           | @List_skipn A => Raw.ident.List_skipn
+           | @List_repeat A => Raw.ident.List_repeat
+           | @List_combine A B => Raw.ident.List_combine
+           | @List_map A B => Raw.ident.List_map
+           | @List_app A => Raw.ident.List_app
+           | @List_rev A => Raw.ident.List_rev
+           | @List_flat_map A B => Raw.ident.List_flat_map
+           | @List_partition A => Raw.ident.List_partition
+           | @List_fold_right A B => Raw.ident.List_fold_right
+           | @List_update_nth T => Raw.ident.List_update_nth
+           | @List_nth_default T => Raw.ident.List_nth_default
+           | @Z_add => Raw.ident.Z_add
+           | @Z_mul => Raw.ident.Z_mul
+           | @Z_pow => Raw.ident.Z_pow
+           | @Z_sub => Raw.ident.Z_sub
+           | @Z_opp => Raw.ident.Z_opp
+           | @Z_div => Raw.ident.Z_div
+           | @Z_modulo => Raw.ident.Z_modulo
+           | @Z_log2 => Raw.ident.Z_log2
+           | @Z_log2_up => Raw.ident.Z_log2_up
+           | @Z_eqb => Raw.ident.Z_eqb
+           | @Z_leb => Raw.ident.Z_leb
+           | @Z_geb => Raw.ident.Z_geb
+           | @Z_of_nat => Raw.ident.Z_of_nat
+           | @Z_to_nat => Raw.ident.Z_to_nat
+           | @Z_shiftr => Raw.ident.Z_shiftr
+           | @Z_shiftl => Raw.ident.Z_shiftl
+           | @Z_land => Raw.ident.Z_land
+           | @Z_lor => Raw.ident.Z_lor
+           | @Z_bneg => Raw.ident.Z_bneg
+           | @Z_lnot_modulo => Raw.ident.Z_lnot_modulo
+           | @Z_mul_split => Raw.ident.Z_mul_split
+           | @Z_add_get_carry => Raw.ident.Z_add_get_carry
+           | @Z_add_with_carry => Raw.ident.Z_add_with_carry
+           | @Z_add_with_get_carry => Raw.ident.Z_add_with_get_carry
+           | @Z_sub_get_borrow => Raw.ident.Z_sub_get_borrow
+           | @Z_sub_with_get_borrow => Raw.ident.Z_sub_with_get_borrow
+           | @Z_zselect => Raw.ident.Z_zselect
+           | @Z_add_modulo => Raw.ident.Z_add_modulo
+           | @Z_rshi => Raw.ident.Z_rshi
+           | @Z_cc_m => Raw.ident.Z_cc_m
+           | @Z_cast => Raw.ident.Z_cast
+           | @Z_cast2 => Raw.ident.Z_cast2
+           | @fancy_add => Raw.ident.fancy_add
+           | @fancy_addc => Raw.ident.fancy_addc
+           | @fancy_sub => Raw.ident.fancy_sub
+           | @fancy_subb => Raw.ident.fancy_subb
+           | @fancy_mulll => Raw.ident.fancy_mulll
+           | @fancy_mullh => Raw.ident.fancy_mullh
+           | @fancy_mulhl => Raw.ident.fancy_mulhl
+           | @fancy_mulhh => Raw.ident.fancy_mulhh
+           | @fancy_rshi => Raw.ident.fancy_rshi
+           | @fancy_selc => Raw.ident.fancy_selc
+           | @fancy_selm => Raw.ident.fancy_selm
+           | @fancy_sell => Raw.ident.fancy_sell
+           | @fancy_addm => Raw.ident.fancy_addm
+           end.
+
+      Definition arg_types {t} (idc : ident t) : list Type
+        := match idc return list Type with
+           | @Literal t => [base.interp (Compilers.base.type.type_base t) : Type]
+           | @Nat_succ => []
+           | @Nat_pred => []
+           | @Nat_max => []
+           | @Nat_mul => []
+           | @Nat_add => []
+           | @Nat_sub => []
+           | @nil t => []
+           | @cons t => []
+           | @pair A B => []
+           | @fst A B => []
+           | @snd A B => []
+           | @prod_rect A B T => []
+           | @bool_rect T => []
+           | @nat_rect P => []
+           | @nat_rect_arrow P Q => []
+           | @list_rect A P => []
+           | @list_case A P => []
+           | @List_length T => []
+           | @List_seq => []
+           | @List_firstn A => []
+           | @List_skipn A => []
+           | @List_repeat A => []
+           | @List_combine A B => []
+           | @List_map A B => []
+           | @List_app A => []
+           | @List_rev A => []
+           | @List_flat_map A B => []
+           | @List_partition A => []
+           | @List_fold_right A B => []
+           | @List_update_nth T => []
+           | @List_nth_default T => []
+           | @Z_add => []
+           | @Z_mul => []
+           | @Z_pow => []
+           | @Z_sub => []
+           | @Z_opp => []
+           | @Z_div => []
+           | @Z_modulo => []
+           | @Z_log2 => []
+           | @Z_log2_up => []
+           | @Z_eqb => []
+           | @Z_leb => []
+           | @Z_geb => []
+           | @Z_of_nat => []
+           | @Z_to_nat => []
+           | @Z_shiftr => []
+           | @Z_shiftl => []
+           | @Z_land => []
+           | @Z_lor => []
+           | @Z_bneg => []
+           | @Z_lnot_modulo => []
+           | @Z_mul_split => []
+           | @Z_add_get_carry => []
+           | @Z_add_with_carry => []
+           | @Z_add_with_get_carry => []
+           | @Z_sub_get_borrow => []
+           | @Z_sub_with_get_borrow => []
+           | @Z_zselect => []
+           | @Z_add_modulo => []
+           | @Z_rshi => []
+           | @Z_cc_m => []
+           | @Z_cast => [zrange : Type]
+           | @Z_cast2 => [zrange * zrange : Type]
+           | @fancy_add => [Z : Type; Z : Type]
+           | @fancy_addc => [Z : Type; Z : Type]
+           | @fancy_sub => [Z : Type; Z : Type]
+           | @fancy_subb => [Z : Type; Z : Type]
+           | @fancy_mulll => [Z : Type]
+           | @fancy_mullh => [Z : Type]
+           | @fancy_mulhl => [Z : Type]
+           | @fancy_mulhh => [Z : Type]
+           | @fancy_rshi => [Z : Type; Z : Type]
+           | @fancy_selc => []
+           | @fancy_selm => [Z : Type]
+           | @fancy_sell => []
+           | @fancy_addm => []
+           end%type.
+
+      Definition to_typed {t} (idc : ident t) (evm : EvarMap) : type_of_list (arg_types idc) -> Compilers.ident.ident (pattern.type.subst_default t evm)
+        := match idc in ident t return type_of_list (arg_types idc) -> Compilers.ident.ident (pattern.type.subst_default t evm) with
+           | @Literal t => fun arg => let '(v, _) := eta2r arg in @Compilers.ident.Literal _ v
+           | @Nat_succ => fun _ => @Compilers.ident.Nat_succ
+           | @Nat_pred => fun _ => @Compilers.ident.Nat_pred
+           | @Nat_max => fun _ => @Compilers.ident.Nat_max
+           | @Nat_mul => fun _ => @Compilers.ident.Nat_mul
+           | @Nat_add => fun _ => @Compilers.ident.Nat_add
+           | @Nat_sub => fun _ => @Compilers.ident.Nat_sub
+           | @nil t => fun _ => @Compilers.ident.nil _
+           | @cons t => fun _ => @Compilers.ident.cons _
+           | @pair A B => fun _ => @Compilers.ident.pair _ _
+           | @fst A B => fun _ => @Compilers.ident.fst _ _
+           | @snd A B => fun _ => @Compilers.ident.snd _ _
+           | @prod_rect A B T => fun _ => @Compilers.ident.prod_rect _ _ _
+           | @bool_rect T => fun _ => @Compilers.ident.bool_rect _
+           | @nat_rect P => fun _ => @Compilers.ident.nat_rect _
+           | @nat_rect_arrow P Q => fun _ => @Compilers.ident.nat_rect_arrow _ _
+           | @list_rect A P => fun _ => @Compilers.ident.list_rect _ _
+           | @list_case A P => fun _ => @Compilers.ident.list_case _ _
+           | @List_length T => fun _ => @Compilers.ident.List_length _
+           | @List_seq => fun _ => @Compilers.ident.List_seq
+           | @List_firstn A => fun _ => @Compilers.ident.List_firstn _
+           | @List_skipn A => fun _ => @Compilers.ident.List_skipn _
+           | @List_repeat A => fun _ => @Compilers.ident.List_repeat _
+           | @List_combine A B => fun _ => @Compilers.ident.List_combine _ _
+           | @List_map A B => fun _ => @Compilers.ident.List_map _ _
+           | @List_app A => fun _ => @Compilers.ident.List_app _
+           | @List_rev A => fun _ => @Compilers.ident.List_rev _
+           | @List_flat_map A B => fun _ => @Compilers.ident.List_flat_map _ _
+           | @List_partition A => fun _ => @Compilers.ident.List_partition _
+           | @List_fold_right A B => fun _ => @Compilers.ident.List_fold_right _ _
+           | @List_update_nth T => fun _ => @Compilers.ident.List_update_nth _
+           | @List_nth_default T => fun _ => @Compilers.ident.List_nth_default _
+           | @Z_add => fun _ => @Compilers.ident.Z_add
+           | @Z_mul => fun _ => @Compilers.ident.Z_mul
+           | @Z_pow => fun _ => @Compilers.ident.Z_pow
+           | @Z_sub => fun _ => @Compilers.ident.Z_sub
+           | @Z_opp => fun _ => @Compilers.ident.Z_opp
+           | @Z_div => fun _ => @Compilers.ident.Z_div
+           | @Z_modulo => fun _ => @Compilers.ident.Z_modulo
+           | @Z_log2 => fun _ => @Compilers.ident.Z_log2
+           | @Z_log2_up => fun _ => @Compilers.ident.Z_log2_up
+           | @Z_eqb => fun _ => @Compilers.ident.Z_eqb
+           | @Z_leb => fun _ => @Compilers.ident.Z_leb
+           | @Z_geb => fun _ => @Compilers.ident.Z_geb
+           | @Z_of_nat => fun _ => @Compilers.ident.Z_of_nat
+           | @Z_to_nat => fun _ => @Compilers.ident.Z_to_nat
+           | @Z_shiftr => fun _ => @Compilers.ident.Z_shiftr
+           | @Z_shiftl => fun _ => @Compilers.ident.Z_shiftl
+           | @Z_land => fun _ => @Compilers.ident.Z_land
+           | @Z_lor => fun _ => @Compilers.ident.Z_lor
+           | @Z_bneg => fun _ => @Compilers.ident.Z_bneg
+           | @Z_lnot_modulo => fun _ => @Compilers.ident.Z_lnot_modulo
+           | @Z_mul_split => fun _ => @Compilers.ident.Z_mul_split
+           | @Z_add_get_carry => fun _ => @Compilers.ident.Z_add_get_carry
+           | @Z_add_with_carry => fun _ => @Compilers.ident.Z_add_with_carry
+           | @Z_add_with_get_carry => fun _ => @Compilers.ident.Z_add_with_get_carry
+           | @Z_sub_get_borrow => fun _ => @Compilers.ident.Z_sub_get_borrow
+           | @Z_sub_with_get_borrow => fun _ => @Compilers.ident.Z_sub_with_get_borrow
+           | @Z_zselect => fun _ => @Compilers.ident.Z_zselect
+           | @Z_add_modulo => fun _ => @Compilers.ident.Z_add_modulo
+           | @Z_rshi => fun _ => @Compilers.ident.Z_rshi
+           | @Z_cc_m => fun _ => @Compilers.ident.Z_cc_m
+           | @Z_cast => fun arg => let '(range, _) := eta2r arg in @Compilers.ident.Z_cast range
+           | @Z_cast2 => fun arg => let '(range, _) := eta2r arg in @Compilers.ident.Z_cast2 range
+           | @fancy_add => fun arg => let '(log2wordmax, (imm, _)) := eta3r arg in @Compilers.ident.fancy_add log2wordmax imm
+           | @fancy_addc => fun arg => let '(log2wordmax, (imm, _)) := eta3r arg in @Compilers.ident.fancy_addc log2wordmax imm
+           | @fancy_sub => fun arg => let '(log2wordmax, (imm, _)) := eta3r arg in @Compilers.ident.fancy_sub log2wordmax imm
+           | @fancy_subb => fun arg => let '(log2wordmax, (imm, _)) := eta3r arg in @Compilers.ident.fancy_subb log2wordmax imm
+           | @fancy_mulll => fun arg => let '(log2wordmax, _) := eta2r arg in @Compilers.ident.fancy_mulll log2wordmax
+           | @fancy_mullh => fun arg => let '(log2wordmax, _) := eta2r arg in @Compilers.ident.fancy_mullh log2wordmax
+           | @fancy_mulhl => fun arg => let '(log2wordmax, _) := eta2r arg in @Compilers.ident.fancy_mulhl log2wordmax
+           | @fancy_mulhh => fun arg => let '(log2wordmax, _) := eta2r arg in @Compilers.ident.fancy_mulhh log2wordmax
+           | @fancy_rshi => fun arg => let '(log2wordmax, (x, _)) := eta3r arg in @Compilers.ident.fancy_rshi log2wordmax x
+           | @fancy_selc => fun _ => @Compilers.ident.fancy_selc
+           | @fancy_selm => fun arg => let '(log2wordmax, _) := eta2r arg in @Compilers.ident.fancy_selm log2wordmax
+           | @fancy_sell => fun _ => @Compilers.ident.fancy_sell
+           | @fancy_addm => fun _ => @Compilers.ident.fancy_addm
+           end.
+
+      Definition unify {t t'} (pidc : ident t) (idc : Compilers.ident.ident t') : option (type_of_list (@arg_types t pidc))
+        := match pidc, idc return option (type_of_list (arg_types pidc)) with
+           | @Literal Compilers.base.type.unit, Compilers.ident.Literal Compilers.base.type.unit v => Some (v, tt)
+           | @Literal Compilers.base.type.Z, Compilers.ident.Literal Compilers.base.type.Z v => Some (v, tt)
+           | @Literal Compilers.base.type.bool, Compilers.ident.Literal Compilers.base.type.bool v => Some (v, tt)
+           | @Literal Compilers.base.type.nat, Compilers.ident.Literal Compilers.base.type.nat v => Some (v, tt)
+           | @Nat_succ, Compilers.ident.Nat_succ => Some tt
+           | @Nat_pred, Compilers.ident.Nat_pred => Some tt
+           | @Nat_max, Compilers.ident.Nat_max => Some tt
+           | @Nat_mul, Compilers.ident.Nat_mul => Some tt
+           | @Nat_add, Compilers.ident.Nat_add => Some tt
+           | @Nat_sub, Compilers.ident.Nat_sub => Some tt
+           | @nil t, Compilers.ident.nil t' => Some tt
+           | @cons t, Compilers.ident.cons t' => Some tt
+           | @pair A B, Compilers.ident.pair A' B' => Some tt
+           | @fst A B, Compilers.ident.fst A' B' => Some tt
+           | @snd A B, Compilers.ident.snd A' B' => Some tt
+           | @prod_rect A B T, Compilers.ident.prod_rect A' B' T' => Some tt
+           | @bool_rect T, Compilers.ident.bool_rect T' => Some tt
+           | @nat_rect P, Compilers.ident.nat_rect P' => Some tt
+           | @nat_rect_arrow P Q, Compilers.ident.nat_rect_arrow P' Q' => Some tt
+           | @list_rect A P, Compilers.ident.list_rect A' P' => Some tt
+           | @list_case A P, Compilers.ident.list_case A' P' => Some tt
+           | @List_length T, Compilers.ident.List_length T' => Some tt
+           | @List_seq, Compilers.ident.List_seq => Some tt
+           | @List_firstn A, Compilers.ident.List_firstn A' => Some tt
+           | @List_skipn A, Compilers.ident.List_skipn A' => Some tt
+           | @List_repeat A, Compilers.ident.List_repeat A' => Some tt
+           | @List_combine A B, Compilers.ident.List_combine A' B' => Some tt
+           | @List_map A B, Compilers.ident.List_map A' B' => Some tt
+           | @List_app A, Compilers.ident.List_app A' => Some tt
+           | @List_rev A, Compilers.ident.List_rev A' => Some tt
+           | @List_flat_map A B, Compilers.ident.List_flat_map A' B' => Some tt
+           | @List_partition A, Compilers.ident.List_partition A' => Some tt
+           | @List_fold_right A B, Compilers.ident.List_fold_right A' B' => Some tt
+           | @List_update_nth T, Compilers.ident.List_update_nth T' => Some tt
+           | @List_nth_default T, Compilers.ident.List_nth_default T' => Some tt
+           | @Z_add, Compilers.ident.Z_add => Some tt
+           | @Z_mul, Compilers.ident.Z_mul => Some tt
+           | @Z_pow, Compilers.ident.Z_pow => Some tt
+           | @Z_sub, Compilers.ident.Z_sub => Some tt
+           | @Z_opp, Compilers.ident.Z_opp => Some tt
+           | @Z_div, Compilers.ident.Z_div => Some tt
+           | @Z_modulo, Compilers.ident.Z_modulo => Some tt
+           | @Z_log2, Compilers.ident.Z_log2 => Some tt
+           | @Z_log2_up, Compilers.ident.Z_log2_up => Some tt
+           | @Z_eqb, Compilers.ident.Z_eqb => Some tt
+           | @Z_leb, Compilers.ident.Z_leb => Some tt
+           | @Z_geb, Compilers.ident.Z_geb => Some tt
+           | @Z_of_nat, Compilers.ident.Z_of_nat => Some tt
+           | @Z_to_nat, Compilers.ident.Z_to_nat => Some tt
+           | @Z_shiftr, Compilers.ident.Z_shiftr => Some tt
+           | @Z_shiftl, Compilers.ident.Z_shiftl => Some tt
+           | @Z_land, Compilers.ident.Z_land => Some tt
+           | @Z_lor, Compilers.ident.Z_lor => Some tt
+           | @Z_bneg, Compilers.ident.Z_bneg => Some tt
+           | @Z_lnot_modulo, Compilers.ident.Z_lnot_modulo => Some tt
+           | @Z_mul_split, Compilers.ident.Z_mul_split => Some tt
+           | @Z_add_get_carry, Compilers.ident.Z_add_get_carry => Some tt
+           | @Z_add_with_carry, Compilers.ident.Z_add_with_carry => Some tt
+           | @Z_add_with_get_carry, Compilers.ident.Z_add_with_get_carry => Some tt
+           | @Z_sub_get_borrow, Compilers.ident.Z_sub_get_borrow => Some tt
+           | @Z_sub_with_get_borrow, Compilers.ident.Z_sub_with_get_borrow => Some tt
+           | @Z_zselect, Compilers.ident.Z_zselect => Some tt
+           | @Z_add_modulo, Compilers.ident.Z_add_modulo => Some tt
+           | @Z_rshi, Compilers.ident.Z_rshi => Some tt
+           | @Z_cc_m, Compilers.ident.Z_cc_m => Some tt
+           | @Z_cast, Compilers.ident.Z_cast range' => Some (range', tt)
+           | @Z_cast2, Compilers.ident.Z_cast2 range' => Some (range', tt)
+           | @fancy_add, Compilers.ident.fancy_add log2wordmax' imm' => Some (log2wordmax', (imm', tt))
+           | @fancy_addc, Compilers.ident.fancy_addc log2wordmax' imm' => Some (log2wordmax', (imm', tt))
+           | @fancy_sub, Compilers.ident.fancy_sub log2wordmax' imm' => Some (log2wordmax', (imm', tt))
+           | @fancy_subb, Compilers.ident.fancy_subb log2wordmax' imm' => Some (log2wordmax', (imm', tt))
+           | @fancy_mulll, Compilers.ident.fancy_mulll log2wordmax' => Some (log2wordmax', tt)
+           | @fancy_mullh, Compilers.ident.fancy_mullh log2wordmax' => Some (log2wordmax', tt)
+           | @fancy_mulhl, Compilers.ident.fancy_mulhl log2wordmax' => Some (log2wordmax', tt)
+           | @fancy_mulhh, Compilers.ident.fancy_mulhh log2wordmax' => Some (log2wordmax', tt)
+           | @fancy_rshi, Compilers.ident.fancy_rshi log2wordmax' x' => Some (log2wordmax', (x', tt))
+           | @fancy_selc, Compilers.ident.fancy_selc => Some tt
+           | @fancy_selm, Compilers.ident.fancy_selm log2wordmax' => Some (log2wordmax', tt)
+           | @fancy_sell, Compilers.ident.fancy_sell => Some tt
+           | @fancy_addm, Compilers.ident.fancy_addm => Some tt
+           | @Literal _, _
+           | @Nat_succ, _
+           | @Nat_pred, _
+           | @Nat_max, _
+           | @Nat_mul, _
+           | @Nat_add, _
+           | @Nat_sub, _
+           | @nil _, _
+           | @cons _, _
+           | @pair _ _, _
+           | @fst _ _, _
+           | @snd _ _, _
+           | @prod_rect _ _ _, _
+           | @bool_rect _, _
+           | @nat_rect _, _
+           | @nat_rect_arrow _ _, _
+           | @list_rect _ _, _
+           | @list_case _ _, _
+           | @List_length _, _
+           | @List_seq, _
+           | @List_firstn _, _
+           | @List_skipn _, _
+           | @List_repeat _, _
+           | @List_combine _ _, _
+           | @List_map _ _, _
+           | @List_app _, _
+           | @List_rev _, _
+           | @List_flat_map _ _, _
+           | @List_partition _, _
+           | @List_fold_right _ _, _
+           | @List_update_nth _, _
+           | @List_nth_default _, _
+           | @Z_add, _
+           | @Z_mul, _
+           | @Z_pow, _
+           | @Z_sub, _
+           | @Z_opp, _
+           | @Z_div, _
+           | @Z_modulo, _
+           | @Z_log2, _
+           | @Z_log2_up, _
+           | @Z_eqb, _
+           | @Z_leb, _
+           | @Z_geb, _
+           | @Z_of_nat, _
+           | @Z_to_nat, _
+           | @Z_shiftr, _
+           | @Z_shiftl, _
+           | @Z_land, _
+           | @Z_lor, _
+           | @Z_bneg, _
+           | @Z_lnot_modulo, _
+           | @Z_mul_split, _
+           | @Z_add_get_carry, _
+           | @Z_add_with_carry, _
+           | @Z_add_with_get_carry, _
+           | @Z_sub_get_borrow, _
+           | @Z_sub_with_get_borrow, _
+           | @Z_zselect, _
+           | @Z_add_modulo, _
+           | @Z_rshi, _
+           | @Z_cc_m, _
+           | @Z_cast, _
+           | @Z_cast2, _
+           | @fancy_add, _
+           | @fancy_addc, _
+           | @fancy_sub, _
+           | @fancy_subb, _
+           | @fancy_mulll, _
+           | @fancy_mullh, _
+           | @fancy_mulhl, _
+           | @fancy_mulhh, _
+           | @fancy_rshi, _
+           | @fancy_selc, _
+           | @fancy_selm, _
+           | @fancy_sell, _
+           | @fancy_addm, _
+             => None
+           end%cps.
+
+      Definition of_typed_ident {t} (idc : Compilers.ident.ident t) : ident (type.relax t)
+        := match idc with
+           | Compilers.ident.Literal t v => @Literal t
+           | Compilers.ident.Nat_succ => @Nat_succ
+           | Compilers.ident.Nat_pred => @Nat_pred
+           | Compilers.ident.Nat_max => @Nat_max
+           | Compilers.ident.Nat_mul => @Nat_mul
+           | Compilers.ident.Nat_add => @Nat_add
+           | Compilers.ident.Nat_sub => @Nat_sub
+           | Compilers.ident.nil t => @nil (base.relax t)
+           | Compilers.ident.cons t => @cons (base.relax t)
+           | Compilers.ident.pair A B => @pair (base.relax A) (base.relax B)
+           | Compilers.ident.fst A B => @fst (base.relax A) (base.relax B)
+           | Compilers.ident.snd A B => @snd (base.relax A) (base.relax B)
+           | Compilers.ident.prod_rect A B T => @prod_rect (base.relax A) (base.relax B) (base.relax T)
+           | Compilers.ident.bool_rect T => @bool_rect (base.relax T)
+           | Compilers.ident.nat_rect P => @nat_rect (base.relax P)
+           | Compilers.ident.nat_rect_arrow P Q => @nat_rect_arrow (base.relax P) (base.relax Q)
+           | Compilers.ident.list_rect A P => @list_rect (base.relax A) (base.relax P)
+           | Compilers.ident.list_case A P => @list_case (base.relax A) (base.relax P)
+           | Compilers.ident.List_length T => @List_length (base.relax T)
+           | Compilers.ident.List_seq => @List_seq
+           | Compilers.ident.List_firstn A => @List_firstn (base.relax A)
+           | Compilers.ident.List_skipn A => @List_skipn (base.relax A)
+           | Compilers.ident.List_repeat A => @List_repeat (base.relax A)
+           | Compilers.ident.List_combine A B => @List_combine (base.relax A) (base.relax B)
+           | Compilers.ident.List_map A B => @List_map (base.relax A) (base.relax B)
+           | Compilers.ident.List_app A => @List_app (base.relax A)
+           | Compilers.ident.List_rev A => @List_rev (base.relax A)
+           | Compilers.ident.List_flat_map A B => @List_flat_map (base.relax A) (base.relax B)
+           | Compilers.ident.List_partition A => @List_partition (base.relax A)
+           | Compilers.ident.List_fold_right A B => @List_fold_right (base.relax A) (base.relax B)
+           | Compilers.ident.List_update_nth T => @List_update_nth (base.relax T)
+           | Compilers.ident.List_nth_default T => @List_nth_default (base.relax T)
+           | Compilers.ident.Z_add => @Z_add
+           | Compilers.ident.Z_mul => @Z_mul
+           | Compilers.ident.Z_pow => @Z_pow
+           | Compilers.ident.Z_sub => @Z_sub
+           | Compilers.ident.Z_opp => @Z_opp
+           | Compilers.ident.Z_div => @Z_div
+           | Compilers.ident.Z_modulo => @Z_modulo
+           | Compilers.ident.Z_log2 => @Z_log2
+           | Compilers.ident.Z_log2_up => @Z_log2_up
+           | Compilers.ident.Z_eqb => @Z_eqb
+           | Compilers.ident.Z_leb => @Z_leb
+           | Compilers.ident.Z_geb => @Z_geb
+           | Compilers.ident.Z_of_nat => @Z_of_nat
+           | Compilers.ident.Z_to_nat => @Z_to_nat
+           | Compilers.ident.Z_shiftr => @Z_shiftr
+           | Compilers.ident.Z_shiftl => @Z_shiftl
+           | Compilers.ident.Z_land => @Z_land
+           | Compilers.ident.Z_lor => @Z_lor
+           | Compilers.ident.Z_bneg => @Z_bneg
+           | Compilers.ident.Z_lnot_modulo => @Z_lnot_modulo
+           | Compilers.ident.Z_mul_split => @Z_mul_split
+           | Compilers.ident.Z_add_get_carry => @Z_add_get_carry
+           | Compilers.ident.Z_add_with_carry => @Z_add_with_carry
+           | Compilers.ident.Z_add_with_get_carry => @Z_add_with_get_carry
+           | Compilers.ident.Z_sub_get_borrow => @Z_sub_get_borrow
+           | Compilers.ident.Z_sub_with_get_borrow => @Z_sub_with_get_borrow
+           | Compilers.ident.Z_zselect => @Z_zselect
+           | Compilers.ident.Z_add_modulo => @Z_add_modulo
+           | Compilers.ident.Z_rshi => @Z_rshi
+           | Compilers.ident.Z_cc_m => @Z_cc_m
+           | Compilers.ident.Z_cast range => @Z_cast
+           | Compilers.ident.Z_cast2 range => @Z_cast2
+           | Compilers.ident.fancy_add log2wordmax imm => @fancy_add
+           | Compilers.ident.fancy_addc log2wordmax imm => @fancy_addc
+           | Compilers.ident.fancy_sub log2wordmax imm => @fancy_sub
+           | Compilers.ident.fancy_subb log2wordmax imm => @fancy_subb
+           | Compilers.ident.fancy_mulll log2wordmax => @fancy_mulll
+           | Compilers.ident.fancy_mullh log2wordmax => @fancy_mullh
+           | Compilers.ident.fancy_mulhl log2wordmax => @fancy_mulhl
+           | Compilers.ident.fancy_mulhh log2wordmax => @fancy_mulhh
+           | Compilers.ident.fancy_rshi log2wordmax x => @fancy_rshi
+           | Compilers.ident.fancy_selc => @fancy_selc
+           | Compilers.ident.fancy_selm log2wordmax => @fancy_selm
+           | Compilers.ident.fancy_sell => @fancy_sell
+           | Compilers.ident.fancy_addm => @fancy_addm
+           end.
+
+    End ident.
+
+    (*===*)
+
+  End pattern.
+End Compilers.