From 0bbbdfede48aed7a74ac2fb95440256ed60fb6e8 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 1 Feb 2019 18:17:11 -0500
Subject: Add support for reifying `zrange` and `option`

This is needed to reify statements for the rewriter.
---
 src/AbstractInterpretation.v                 |  98 ++++-
 src/AbstractInterpretationProofs.v           |  49 ++-
 src/AbstractInterpretationWf.v               |  72 +++-
 src/AbstractInterpretationZRangeProofs.v     |  11 +-
 src/BoundsPipeline.v                         |  14 +
 src/CStringification.v                       | 111 ++++-
 src/CompilersTestCases.v                     |   4 +-
 src/GENERATEDIdentifiersWithoutTypes.v       | 594 ++++++++++++++++++---------
 src/GENERATEDIdentifiersWithoutTypesProofs.v |  32 +-
 src/Language.v                               | 199 ++++++---
 src/LanguageInversion.v                      |  44 ++
 src/LanguageWf.v                             |  63 ++-
 src/Rewriter.v                               |  27 +-
 src/RewriterWf1.v                            |   2 +
 src/UnderLets.v                              |  24 ++
 src/UnderLetsProofs.v                        |   9 +-
 16 files changed, 1010 insertions(+), 343 deletions(-)

diff --git a/src/AbstractInterpretation.v b/src/AbstractInterpretation.v
index 75ce71eff..63a7df1ed 100644
--- a/src/AbstractInterpretation.v
+++ b/src/AbstractInterpretation.v
@@ -29,9 +29,11 @@ Module Compilers.
              | base.type.unit as t
              | base.type.nat as t
              | base.type.bool as t
+             | base.type.zrange as t
                => base.interp t
              | base.type.prod A B => interp A * interp B
              | base.type.list A => list (interp A)
+             | base.type.option A => option (interp A)
              end%type.
         Definition is_neg {t} : interp t -> bool
           := match t with
@@ -44,11 +46,14 @@ Module Compilers.
              | base.type.nat => Nat.eqb
              | base.type.unit => fun _ _ => true
              | base.type.bool => bool_eq
+             | base.type.zrange => zrange_beq
              | base.type.prod A B
                => fun '(a, b) '(a', b')
                   => @is_tighter_than A a a' && @is_tighter_than B b b'
              | base.type.list A
                => fold_andb_map (@is_tighter_than A)
+             | base.type.option A
+               => option_beq (@is_tighter_than A)
              end%bool.
         Fixpoint is_bounded_by {t} : interp t -> binterp t -> bool
           := match t with
@@ -56,11 +61,14 @@ Module Compilers.
              | base.type.nat => Nat.eqb
              | base.type.unit => fun _ _ => true
              | base.type.bool => bool_eq
+             | base.type.zrange => zrange_beq
              | base.type.prod A B
                => fun '(a, b) '(a', b')
                   => @is_bounded_by A a a' && @is_bounded_by B b b'
              | base.type.list A
                => fold_andb_map (@is_bounded_by A)
+             | base.type.option A
+               => option_beq_hetero (@is_bounded_by A)
              end.
         Module option.
           (** turn a [base.type] into a [Set] describing the type
@@ -73,44 +81,55 @@ Module Compilers.
                | base.type.unit => unit
                | base.type.nat as t
                | base.type.bool as t
+               | base.type.zrange as t
                  => option (base.interp t)
                | base.type.prod A B => interp A * interp B
                | base.type.list A => option (list (interp A))
+               | base.type.option A => option (option (interp A))
                end%type.
           Fixpoint None {t} : interp t
             := match t with
                | base.type.unit => tt
                | base.type.list _
+               | base.type.option _
                | base.type.Z
                | base.type.nat
                | base.type.bool
+               | base.type.zrange
                  => Datatypes.None
                | base.type.prod A B
                  => (@None A, @None B)
                end.
           Fixpoint Some {t} : base.interp t -> interp t
             := match t with
+               | base.type.unit
+                 => fun _ => tt
                | base.type.Z
                | base.type.nat
                | base.type.bool
+               | base.type.zrange
                  => Datatypes.Some
                | base.type.list A
                  => fun ls => Datatypes.Some (List.map (@Some A) ls)
+               | base.type.option A
+                 => fun ls => Datatypes.Some (option_map (@Some A) ls)
                | base.type.prod A B
                  => fun '(a, b)
                     => (@Some A a, @Some B b)
-               | _ => fun _ => tt
                end.
           Fixpoint lift_Some {t} : interp t -> option (base.interp t)
             := match t with
                | base.type.Z
                | base.type.nat
                | base.type.bool
+               | base.type.zrange
                  => fun x => x
                | base.type.unit
                  => fun x => Datatypes.Some tt
                | base.type.list A
-                 => fun ls => ls <- ls; ls <-- List.map (@lift_Some A) ls; Datatypes.Some ls
+                 => fun ls => ls <- ls; Option.List.lift (List.map (@lift_Some A) ls)
+               | base.type.option A
+                 => fun v => v <- v; Option.lift (option_map (@lift_Some A) v)
                | base.type.prod A B
                  => fun '(a, b) => a <- @lift_Some A a; b <- @lift_Some B b; Datatypes.Some (a, b)
                end%option.
@@ -121,9 +140,12 @@ Module Compilers.
                | base.type.nat
                | base.type.bool
                | base.type.unit
+               | base.type.zrange
                  => fun x => x
                | base.type.list A
                  => fun ls => ls <- ls; Datatypes.Some (List.map (@strip_ranges A) ls)
+               | base.type.option A
+                 => fun v => v <- v; Datatypes.Some (option_map (@strip_ranges A) v)
                | base.type.prod A B
                  => fun '(a, b)
                     => (@strip_ranges A a, @strip_ranges B b)
@@ -142,6 +164,7 @@ Module Compilers.
                | base.type.Z as t
                | base.type.nat as t
                | base.type.bool as t
+               | base.type.zrange as t
                  => fun r1 r2
                     => match r1, r2 with
                        | _, Datatypes.None => true
@@ -159,6 +182,14 @@ Module Compilers.
                        | Datatypes.None, Datatypes.Some _ => false
                        | Datatypes.Some ls1, Datatypes.Some ls2 => fold_andb_map (@is_tighter_than A) ls1 ls2
                        end
+               | base.type.option A
+                 => fun v1 v2
+                    => match v1, v2 with
+                       | Datatypes.None, Datatypes.None => true
+                       | Datatypes.Some _, Datatypes.None => true
+                       | Datatypes.None, Datatypes.Some _ => false
+                       | Datatypes.Some v1, Datatypes.Some v2 => option_beq (@is_tighter_than A) v1 v2
+                       end
                | _ => fun 'tt 'tt => true
                end.
           Fixpoint is_bounded_by {t} : interp t -> binterp t -> bool
@@ -166,6 +197,7 @@ Module Compilers.
                | base.type.Z as t
                | base.type.nat as t
                | base.type.bool as t
+               | base.type.zrange as t
                  => fun r
                     => match r with
                        | Datatypes.Some r => @base.is_bounded_by t r
@@ -180,6 +212,12 @@ Module Compilers.
                        | Datatypes.None => true
                        | Datatypes.Some ls1 => fold_andb_map (@is_bounded_by A) ls1 ls2
                        end
+               | base.type.option A
+                 => fun v1 v2
+                    => match v1 with
+                       | Datatypes.None => true
+                       | Datatypes.Some v1 => option_beq_hetero (@is_bounded_by A) v1 v2
+                       end
                | _ => fun 'tt _ => true
                end.
 
@@ -191,6 +229,7 @@ Module Compilers.
                            | progress cbn in *
                            | progress destruct_head'_prod
                            | progress destruct_head' base.type.base
+                           | progress destruct_head' option
                            | rewrite fold_andb_map_map1
                            | match goal with H : _ |- _ => rewrite H end
                            | match goal with H : _ |- _ => setoid_rewrite H end ].
@@ -216,10 +255,12 @@ Module Compilers.
                            | progress break_innermost_match_hyps
                            | progress subst
                            | rewrite NPeano.Nat.eqb_refl
+                           | apply zrange_lb
                            | reflexivity
                            | match goal with
                              | [ H : Nat.eqb _ _ = true |- _ ] => apply beq_nat_true in H
                              | [ H : bool_eq _ _ = true |- _ ] => apply bool_eq_ok in H
+                             | [ H : zrange_beq _ _ = true |- _ ] => apply zrange_bl in H
                              | [ |- bool_eq ?x ?x = true ] => destruct x; reflexivity
                              end ].
             { lazymatch goal with
@@ -325,6 +366,7 @@ Module Compilers.
              | base.type.Z => fun z => Some r[z~>z]%zrange
              | base.type.nat
              | base.type.bool
+             | base.type.zrange
                => fun n => Some n
              | base.type.unit
                => fun _ => tt
@@ -332,21 +374,24 @@ Module Compilers.
                => fun '(a, b) => (@of_literal A a, @of_literal B b)
              | base.type.list A
                => fun ls => Some (List.map (@of_literal A) ls)
+             | base.type.option A
+               => fun v => Some (option_map (@of_literal A) v)
              end.
         Fixpoint to_literal {t} : type.base.option.interp t -> option (base.interp t)
           := match t with
              | base.type.Z => fun r => r <- r; if r.(lower) =? r.(upper) then Some r.(lower) else None
              | base.type.nat
              | base.type.bool
+             | base.type.zrange
                => fun v => v
              | base.type.unit
                => fun _ => Some tt
              | base.type.prod A B
                => fun '(a, b) => a <- @to_literal A a; b <- @to_literal B b; Some (a, b)
              | base.type.list A
-               => fun ls => ls <- ls; fold_right (fun x xs => x <- x; xs <- xs; Some (x :: xs))
-                                                 (Some nil)
-                                                 (List.map (@to_literal A) ls)
+               => fun ls => ls <- ls; Option.List.lift (List.map (@to_literal A) ls)
+             | base.type.option A
+               => fun v => v <- v; Option.lift (option_map (@to_literal A) v)
              end%option%Z.
         Local Notation rSome v
           := (ZRange.type.base.option.Some (t:=base.reify_norm_type_of v) v)
@@ -414,9 +459,14 @@ Module Compilers.
                    end
              | ident.Z_eqb as idc
              | ident.Z_leb as idc
+             | ident.Z_ltb as idc
              | ident.Z_geb as idc
+             | ident.Z_gtb as idc
+             | ident.Z_max as idc
+             | ident.Z_min as idc
              | ident.Z_pow as idc
              | ident.Z_modulo as idc
+             | ident.Build_zrange as idc
                => fun x y => match to_literal x, to_literal y with
                              | Some x, Some y => of_literal (ident.interp idc x y)
                              | _, _ => ZRange.type.base.option.None
@@ -443,6 +493,21 @@ Module Compilers.
                    | Some b => if b then t tt else f tt
                    | None => ZRange.type.base.option.None
                    end
+             | ident.option_rect _ _
+               => fun s n o
+                 => match o with
+                   | Some o => option_rect _ s (n tt) o
+                   | None => ZRange.type.base.option.None
+                   end
+             | ident.zrange_rect _
+               => fun f v
+                 => match v with
+                    | Some v => ZRange.zrange_rect
+                                  _
+                                  (fun l u => f (Some (ZRange.constant l)) (Some (ZRange.constant u)))
+                                  v
+                   | None => ZRange.type.base.option.None
+                   end
              | ident.nat_rect _
                => fun O_case S_case n
                  => match n with
@@ -506,6 +571,8 @@ Module Compilers.
                => fun n f ls => ls <- ls; n <- n; Some (update_nth n f ls)
              | ident.nil t => Some nil
              | ident.cons t => fun x => option_map (cons x)
+             | ident.None t => Some None
+             | ident.Some t => fun x => Some (Some x)
              | ident.pair A B => pair
              | ident.fst A B => fst
              | ident.snd A B => snd
@@ -837,6 +904,7 @@ Module Compilers.
                 (bottom' : forall A, abstract_domain' A)
                 (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t)
                 (extract_list_state : forall A, abstract_domain' (base.type.list A) -> option (list (abstract_domain' A)))
+                (extract_option_state : forall A, abstract_domain' (base.type.option A) -> option (option (abstract_domain' A)))
                 (is_annotated_for : forall t t', ident t -> abstract_domain' t' -> bool).
 
         (** TODO: Is it okay to commute annotations? *)
@@ -897,6 +965,18 @@ Module Compilers.
                              Base (reify_list retv))
                      | None, _ => annotate_with_ident is_let_bound st e
                      end
+             | base.type.option A
+               => fun st e
+                  => match extract_option_state _ st, reflect_option e with
+                     | Some v_st, Some v_e
+                       => (retv <----- (Option.map
+                                          (fun '(st', e') => @annotate is_let_bound A st' e')
+                                          (Option.combine v_st v_e));
+                             Base (reify_option retv))
+                     | Some _, None
+                     | None, _
+                       => annotate_with_ident is_let_bound st e
+                     end
              end%under_lets.
 
         Local Notation value_with_lets := (@value_with_lets base.type ident var abstract_domain').
@@ -1001,14 +1081,16 @@ Module Compilers.
           := ZRange.ident.option.interp idc.
         Definition extract_list_state A (st : abstract_domain' (base.type.list A)) : option (list (abstract_domain' A))
           := st.
+        Definition extract_option_state A (st : abstract_domain' (base.type.option A)) : option (option (abstract_domain' A))
+          := st.
 
         Definition eval_with_bound {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
           := (@partial.ident.eval_with_bound)
-               var abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for true t e bound.
+               var abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for true t e bound.
 
         Definition eta_expand_with_bound {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
           := (@partial.ident.eta_expand_with_bound)
-               var abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for t e bound.
+               var abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for t e bound.
 
         Definition EvalWithBound {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
           := fun var => eval_with_bound (e _) bound.
@@ -1018,7 +1100,7 @@ Module Compilers.
 
       Definition eval {var} {t} (e : @expr _ t) : expr t
         := (@partial.ident.eval)
-             var abstract_domain' (annotate_ident default_relax_zrange) bottom' abstract_interp_ident extract_list_state (is_annotated_for default_relax_zrange) t e.
+             var abstract_domain' (annotate_ident default_relax_zrange) bottom' abstract_interp_ident extract_list_state extract_option_state (is_annotated_for default_relax_zrange) t e.
       Definition Eval {t} (e : Expr t) : Expr t
         := fun var => eval (e _).
       Definition EtaExpandWithListInfoFromBound {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
diff --git a/src/AbstractInterpretationProofs.v b/src/AbstractInterpretationProofs.v
index c0f20474d..68df78b13 100644
--- a/src/AbstractInterpretationProofs.v
+++ b/src/AbstractInterpretationProofs.v
@@ -680,6 +680,7 @@ Module Compilers.
                 (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t)
                 (update_literal_with_state : forall A : base.type.base, abstract_domain' A -> base.interp A -> base.interp A)
                 (extract_list_state : forall A, abstract_domain' (base.type.list A) -> option (list (abstract_domain' A)))
+                (extract_option_state : forall A, abstract_domain' (base.type.option A) -> option (option (abstract_domain' A)))
                 (is_annotated_for : forall t t', ident t -> abstract_domain' t' -> bool)
                 (is_annotation : forall t, ident t -> bool)
                 (abstraction_relation' : forall t, abstract_domain' t -> base.interp t -> Prop)
@@ -712,13 +713,18 @@ Module Compilers.
                  : forall t st ls v,
                     extract_list_state t st = Some ls
                     -> abstraction_relation' _ st v
-                    -> length ls = length v).
+                    -> length ls = length v)
+                (extract_option_state_related
+                 : forall t st a v,
+                    extract_option_state t st = Some a
+                    -> abstraction_relation' _ st v
+                    -> option_eq (abstraction_relation' t) a v).
 
         Local Notation update_annotation := (@ident.update_annotation _ abstract_domain' annotate_ident is_annotated_for).
         Local Notation annotate_with_ident := (@ident.annotate_with_ident _ abstract_domain' annotate_ident is_annotated_for).
         Local Notation annotate_base := (@ident.annotate_base _ abstract_domain' annotate_ident is_annotated_for).
-        Local Notation annotate := (@ident.annotate _ abstract_domain' annotate_ident abstract_interp_ident extract_list_state is_annotated_for).
-        Local Notation interp_ident := (@ident.interp_ident _ abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
+        Local Notation annotate := (@ident.annotate _ abstract_domain' annotate_ident abstract_interp_ident extract_list_state extract_option_state is_annotated_for).
+        Local Notation interp_ident := (@ident.interp_ident _ abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for).
         Local Notation related_bounded_value := (@related_bounded_value base.type ident abstract_domain' base.interp (@ident_interp) abstraction_relation' bottom' abstract_domain'_R).
         Local Notation reify := (@reify base.type ident _ abstract_domain' annotate bottom').
         Local Notation reflect := (@reflect base.type ident _ abstract_domain' annotate bottom').
@@ -774,7 +780,7 @@ Module Compilers.
               (He : abstraction_relation' t st (expr.interp (t:=type.base t) (@ident_interp) e))
           : expr.interp (@ident_interp) (UnderLets.interp (@ident_interp) (@annotate is_let_bound t st e))
             = expr.interp (@ident_interp) e.
-        Proof using interp_annotate_ident abstract_interp_ident_Proper' extract_list_state_related extract_list_state_length_good bottom'_related.
+        Proof using interp_annotate_ident abstract_interp_ident_Proper' extract_list_state_related extract_list_state_length_good extract_option_state_related bottom'_related.
           induction t; cbn [annotate]; auto using interp_annotate_base.
           all: repeat first [ reflexivity
                             | progress subst
@@ -834,7 +840,13 @@ Module Compilers.
                             | rewrite <- List.map_map with (f:=fst), map_fst_combine
                             | rewrite Lists.List.firstn_all2 by distr_length
                             | apply map_nth_default_seq
+                            | progress destruct_head' option
+                            | progress cbn [Option.combine option_map reify_option option_rect UnderLets.splice_option] in *
+                            | apply (f_equal Some)
                             | match goal with
+                              | [ H : abstraction_relation' _ ?st _, H' : extract_option_state _ ?st = _ |- _ ]
+                                => eapply extract_option_state_related in H; [ clear H' | eexact H' ];
+                                   cbv [option_eq] in H
                               | [ H : context[expr.interp _ _ = expr.interp _ _] |- expr.interp _ _ = expr.interp _ _ ] => apply H; clear H
                               | [ H : forall st' v', List.In _ (List.combine _ _) -> abstraction_relation' _ _ _ |- abstraction_relation' _ _ _ ]
                                 => apply H; clear H; cbv [List.nth_default]
@@ -844,7 +856,7 @@ Module Compilers.
 
         Lemma interp_ident_Proper_not_nth_default annotate_with_state t idc
           : related_bounded_value (abstract_interp_ident t idc) (UnderLets.interp (@ident_interp) (Base (reflect annotate_with_state (expr.Ident idc) (abstract_interp_ident _ idc)))) (ident_interp idc).
-        Proof using abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_related extract_list_state_length_good extract_list_state_related interp_annotate_ident abstract_interp_ident_Proper bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric.
+        Proof using abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_ident abstract_interp_ident_Proper bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric.
           cbn [UnderLets.interp].
           eapply interp_reflect;
             try first [ apply ident.gen_interp_Proper
@@ -856,7 +868,7 @@ Module Compilers.
 
         Lemma interp_ident_Proper_nth_default annotate_with_state T (idc:=@ident.List_nth_default T)
           : related_bounded_value (abstract_interp_ident _ idc) (UnderLets.interp (@ident_interp) (interp_ident annotate_with_state idc)) (ident_interp idc).
-        Proof using abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper extract_list_state_length_good extract_list_state_related interp_annotate_ident bottom'_related.
+        Proof using abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_ident bottom'_related.
           subst idc; cbn [interp_ident reify reflect fst snd UnderLets.interp ident_interp related_bounded_value abstract_domain value].
           cbv [abstract_domain]; cbn [type.interp bottom_for_each_lhs_of_arrow state_of_value fst snd].
           repeat first [ progress intros
@@ -896,8 +908,8 @@ Module Compilers.
                               | refine (@interp_ident_Proper_nth_default _ _) ].
         Qed.
 
-        Local Notation eval_with_bound := (@partial.ident.eval_with_bound _ abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
-        Local Notation eta_expand_with_bound := (@partial.ident.eta_expand_with_bound _ abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
+        Local Notation eval_with_bound := (@partial.ident.eval_with_bound _ abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for).
+        Local Notation eta_expand_with_bound := (@partial.ident.eta_expand_with_bound _ abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for).
         Local Notation extract := (@ident.extract abstract_domain' bottom' abstract_interp_ident).
 
         Lemma interp_eval_with_bound
@@ -986,6 +998,14 @@ Module Compilers.
           intros; destruct_head'_and; destruct_head'_or; inversion_prod; subst; eauto. }
       Qed.
 
+      Lemma extract_option_state_related {t} st a v
+        : extract_option_state t st = Some a
+          -> @abstraction_relation' _ st v
+          -> option_eq (@abstraction_relation' t) a v.
+      Proof using Type.
+        cbv [abstraction_relation' extract_option_state option_eq]; intros; subst; cbn in *; cbv [option_beq_hetero] in *; break_match; break_match_hyps; auto; congruence.
+      Qed.
+
       Lemma Extract_FromFlat_ToFlat' {t} (e : Expr t) (Hwf : Wf e) b_in1 b_in2
             (Hb : type.and_for_each_lhs_of_arrow (fun t => type.eqv) b_in1 b_in2)
         : partial.Extract (GeneralizeVar.FromFlat (GeneralizeVar.ToFlat e)) b_in1
@@ -1072,7 +1092,7 @@ Module Compilers.
             | intros arg1 Harg11 Harg1 ].
           all: eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1; [ | apply ZRange.type.option.is_bounded_by_impl_related_hetero ].
           all: eapply ident.interp_eval_with_bound with (abstraction_relation':=@abstraction_relation') (abstract_domain'_R:=fun t => abstract_domain'_R t); eauto using bottom'_bottom with typeclass_instances.
-          all: intros; eapply extract_list_state_related; eassumption.
+          all: intros; (eapply extract_list_state_related + eapply extract_option_state_related); eassumption.
         Qed.
 
         Lemma interp_eta_expand_with_bound
@@ -1088,7 +1108,7 @@ Module Compilers.
           cbv [partial.eta_expand_with_bound]; intros arg1 arg2 Harg12 Harg1.
           eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1.
           { apply ident.interp_eta_expand_with_bound with (abstraction_relation':=@abstraction_relation') (abstract_domain'_R:=fun t => abstract_domain'_R t); eauto using bottom'_bottom with typeclass_instances.
-            all: intros; eapply extract_list_state_related; eassumption. }
+            all: intros; (eapply extract_list_state_related + eapply extract_option_state_related); eassumption. }
           { apply ZRange.type.option.is_bounded_by_impl_related_hetero. }
         Qed.
 
@@ -1130,10 +1150,11 @@ Module Compilers.
           -> ZRange.type.option.is_bounded_by (ZRange.type.option.strip_ranges b) v = true.
       Proof using Type.
         induction t as [t|s IHs d IHd]; cbn in *; [ | tauto ].
-        induction t; cbn in *; break_innermost_match; cbn in *; rewrite ?Bool.andb_true_iff; try solve [ intuition ]; [].
-        repeat match goal with ls : list _ |- _ => revert ls end.
-        intros ls1 ls2; revert ls2.
-        induction ls1, ls2; cbn in *; rewrite ?Bool.andb_true_iff; solve [ intuition ].
+        induction t; cbn in *; break_innermost_match; cbn in *; rewrite ?Bool.andb_true_iff; try solve [ intuition ].
+        { repeat match goal with ls : list _ |- _ => revert ls end.
+          intros ls1 ls2; revert ls2.
+          induction ls1, ls2; cbn in *; rewrite ?Bool.andb_true_iff; solve [ intuition ]. }
+        { destruct_head' option; cbn; eauto; congruence. }
       Qed.
 
       Lemma andb_strip_ranges_Proper t (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t) arg1
diff --git a/src/AbstractInterpretationWf.v b/src/AbstractInterpretationWf.v
index 3d9f03f79..a1e2f180e 100644
--- a/src/AbstractInterpretationWf.v
+++ b/src/AbstractInterpretationWf.v
@@ -305,6 +305,7 @@ Module Compilers.
                 (bottom' : forall A, abstract_domain' A)
                 (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t)
                 (extract_list_state : forall A, abstract_domain' (base.type.list A) -> option (list (abstract_domain' A)))
+                (extract_option_state : forall A, abstract_domain' (base.type.option A) -> option (option (abstract_domain' A)))
                 (is_annotated_for : forall t t', ident t -> abstract_domain' t' -> bool).
         Context (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop).
         Local Notation abstract_domain_R := (@abstract_domain_R base.type abstract_domain' abstract_domain'_R).
@@ -313,7 +314,8 @@ Module Compilers.
                 {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)}
                 {is_annotated_for_Proper : forall t t', Proper (eq ==> abstract_domain'_R _ ==> eq) (@is_annotated_for t t')}
                 (extract_list_state_length : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_map (@length _) (extract_list_state t v1) = option_map (@length _) (extract_list_state t v2))
-                (extract_list_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2).
+                (extract_list_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2)
+                (extract_option_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_eq (option_eq (abstract_domain'_R _)) (extract_option_state t v1) (extract_option_state t v2)).
 
         Local Instance abstract_interp_ident_Proper_arrow s d
           : Proper (eq ==> abstract_domain'_R s ==> abstract_domain'_R d) (abstract_interp_ident (type.arrow s d))
@@ -324,14 +326,14 @@ Module Compilers.
 
           Local Notation update_annotation1 := (@ident.update_annotation var1 abstract_domain' annotate_ident is_annotated_for).
           Local Notation update_annotation2 := (@ident.update_annotation var2 abstract_domain' annotate_ident is_annotated_for).
-          Local Notation annotate1 := (@ident.annotate var1 abstract_domain' annotate_ident abstract_interp_ident extract_list_state is_annotated_for).
-          Local Notation annotate2 := (@ident.annotate var2 abstract_domain' annotate_ident abstract_interp_ident extract_list_state is_annotated_for).
+          Local Notation annotate1 := (@ident.annotate var1 abstract_domain' annotate_ident abstract_interp_ident extract_list_state extract_option_state is_annotated_for).
+          Local Notation annotate2 := (@ident.annotate var2 abstract_domain' annotate_ident abstract_interp_ident extract_list_state extract_option_state is_annotated_for).
           Local Notation annotate_base1 := (@ident.annotate_base var1 abstract_domain' annotate_ident is_annotated_for).
           Local Notation annotate_base2 := (@ident.annotate_base var2 abstract_domain' annotate_ident is_annotated_for).
           Local Notation annotate_with_ident1 := (@ident.annotate_with_ident var1 abstract_domain' annotate_ident is_annotated_for).
           Local Notation annotate_with_ident2 := (@ident.annotate_with_ident var2 abstract_domain' annotate_ident is_annotated_for).
-          Local Notation interp_ident1 := (@ident.interp_ident var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
-          Local Notation interp_ident2 := (@ident.interp_ident var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
+          Local Notation interp_ident1 := (@ident.interp_ident var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for).
+          Local Notation interp_ident2 := (@ident.interp_ident var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for).
           Local Notation reflect1 := (@reflect base.type ident var1 abstract_domain' annotate1 bottom').
           Local Notation reflect2 := (@reflect base.type ident var2 abstract_domain' annotate2 bottom').
 
@@ -408,7 +410,7 @@ Module Compilers.
                 v1 v2 (Hv : abstract_domain'_R t v1 v2)
                 e1 e2 (He : expr.wf G e1 e2)
             : UnderLets.wf (fun G' => expr.wf G') G (@annotate1 is_let_bound t v1 e1) (@annotate2 is_let_bound t v2 e2).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper.
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper.
             revert dependent G; induction t; intros;
               cbn [ident.annotate]; try apply wf_annotate_base; trivial.
             all: repeat first [ lazymatch goal with
@@ -430,6 +432,13 @@ Module Compilers.
                                      pose proof (extract_list_state_length _ v1 v2 Hv) as Hl;
                                      pose proof (extract_list_state_rel _ v1 v2 Hv) as Hl';
                                      rewrite H, H' in Hl, Hl'; cbv [option_eq option_map] in Hl, Hl'; clear H H'
+                                | [ H : abstract_domain'_R _ ?v1 ?v2, H1 : extract_option_state _ ?v1 = _, H2 : extract_option_state _ ?v2 = _ |- _ ]
+                                  => let H' := fresh in
+                                     pose proof H as H';
+                                     apply extract_option_state_rel in H';
+                                     rewrite H1, H2 in H';
+                                     cbv [option_eq] in H';
+                                     clear H1 H2
                                 | [ H : ?x = ?x |- _ ] => clear H
                                 | [ H : length ?l1 = length ?l2, H' : context[length ?l1] |- _ ] => rewrite H in H'
                                 end
@@ -476,6 +485,9 @@ Module Compilers.
                               | progress rewrite_type_transport_correct
                               | apply conj
                               | congruence
+                              | progress destruct_head' option
+                              | progress cbn [Option.combine option_map UnderLets.splice_option reify_option option_rect] in *
+                              | progress cbn [type.decode f_equal eq_rect fst snd] in *
                               | solve [ wf_t ] ].
           Qed.
 
@@ -492,7 +504,7 @@ Module Compilers.
             end.
           Lemma wf_interp_ident_nth_default (annotate_with_state : bool) G T
             : wf_value_with_lets G (@interp_ident1 annotate_with_state _ (@ident.List_nth_default T)) (@interp_ident2 annotate_with_state _ (@ident.List_nth_default T)).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper.
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper.
             cbv [wf_value_with_lets wf_value ident.interp_ident]; constructor; cbn -[abstract_domain_R abstract_domain].
             { intros; subst.
               destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *.
@@ -600,7 +612,7 @@ Module Compilers.
 
           Lemma wf_interp_ident_not_nth_default (annotate_with_state : bool) G {t} (idc : ident t)
             : wf_value_with_lets G (Base (reflect1 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc))) (Base (reflect2 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc))).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper.
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper.
             constructor; eapply wf_reflect;
               solve [ apply bottom'_Proper
                     | apply wf_annotate
@@ -610,41 +622,41 @@ Module Compilers.
 
           Lemma wf_interp_ident (annotate_with_state : bool) G {t} idc1 idc2 (Hidc : idc1 = idc2)
             : wf_value_with_lets G (@interp_ident1 annotate_with_state t idc1) (@interp_ident2 annotate_with_state t idc2).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper.
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper.
             cbv [wf_value_with_lets ident.interp_ident]; subst idc2; destruct idc1;
               first [ apply wf_interp_ident_nth_default
                     | apply wf_interp_ident_not_nth_default ].
           Qed.
 
-          Local Notation eval_with_bound1 := (@partial.ident.eval_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
-          Local Notation eval_with_bound2 := (@partial.ident.eval_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
+          Local Notation eval_with_bound1 := (@partial.ident.eval_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for).
+          Local Notation eval_with_bound2 := (@partial.ident.eval_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for).
           Lemma wf_eval_with_bound (annotate_with_state : bool) {t} G G' e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
                 (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
             : expr.wf G' (@eval_with_bound1 annotate_with_state t e1 st1) (@eval_with_bound2 annotate_with_state t e2 st2).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper.
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper.
             eapply wf_eval_with_bound';
               solve [ eassumption
                     | eapply wf_annotate
                     | eapply wf_interp_ident ].
           Qed.
 
-          Local Notation eval1 := (@partial.ident.eval var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
-          Local Notation eval2 := (@partial.ident.eval var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
+          Local Notation eval1 := (@partial.ident.eval var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for).
+          Local Notation eval2 := (@partial.ident.eval var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for).
           Lemma wf_eval {t} G G' e1 e2 (Hwf : expr.wf G e1 e2)
                 (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
             : expr.wf G' (@eval1 t e1) (@eval2 t e2).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper.
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper.
             eapply wf_eval';
               solve [ eassumption
                     | eapply wf_annotate
                     | eapply wf_interp_ident ].
           Qed.
 
-          Local Notation eta_expand_with_bound1 := (@partial.ident.eta_expand_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
-          Local Notation eta_expand_with_bound2 := (@partial.ident.eta_expand_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state is_annotated_for).
+          Local Notation eta_expand_with_bound1 := (@partial.ident.eta_expand_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for).
+          Local Notation eta_expand_with_bound2 := (@partial.ident.eta_expand_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for).
           Lemma wf_eta_expand_with_bound {t} G e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
             : expr.wf G (@eta_expand_with_bound1 t e1 st1) (@eta_expand_with_bound2 t e2 st2).
-          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel is_annotated_for_Proper.
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper.
             eapply wf_eta_expand_with_bound';
               solve [ eassumption
                     | eapply wf_annotate
@@ -682,6 +694,8 @@ Module Compilers.
                        | progress destruct_head'_prod
                        | progress destruct_head'_bool
                        | progress destruct_head' option
+                       | progress inversion_option
+                       | discriminate
                        | solve [ eauto ]
                        | apply NatUtil.nat_rect_Proper_nondep
                        | apply ListUtil.list_rect_Proper
@@ -691,8 +705,15 @@ Module Compilers.
                        | apply ListUtil.update_nth_Proper
                        | apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature)
                        | cbn; apply (f_equal (@Some _))
+                       | progress cbn [ZRange.ident.option.interp]
+                       | progress cbv [zrange_rect]
+                       | apply (f_equal2 pair)
+                       | break_innermost_match_step
                        | match goal with
                          | [ H : _ |- _ ] => erewrite H by (eauto; (eassumption || reflexivity))
+                         | [ H : forall x y, x = y -> _ |- _ ] => specialize (fun x => H x x eq_refl)
+                         | [ H : forall x, ?f x = ?g x, H1 : ?f ?y = _, H2 : ?g ?y = _ |- _ ]
+                           => specialize (H y); rewrite H1, H2 in H
                          end ].
       Qed.
 
@@ -719,6 +740,12 @@ Module Compilers.
         destruct_head'_ex; destruct_head'_and; inversion_prod; subst; reflexivity.
       Qed.
 
+      Lemma extract_option_state_rel
+        : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_eq (option_eq (abstract_domain'_R _)) (extract_option_state t v1) (extract_option_state t v2).
+      Proof.
+        cbv [extract_option_state option_eq]; intros; subst; break_match; reflexivity.
+      Qed.
+
       Section with_var2.
         Context {var1 var2 : type -> Type}.
         Local Notation wf_value_with_lets := (@wf_value_with_lets base.type ident abstract_domain' (fun t => abstract_domain'_R t) var1 var2).
@@ -731,7 +758,8 @@ Module Compilers.
             solve [ eassumption
                   | exact _
                   | apply extract_list_state_length
-                  | apply extract_list_state_rel ].
+                  | apply extract_list_state_rel
+                  | apply extract_option_state_rel ].
         Qed.
 
         Lemma wf_eval_with_bound {relax_zrange t} G G' e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
@@ -742,7 +770,8 @@ Module Compilers.
             solve [ eassumption
                   | exact _
                   | apply extract_list_state_length
-                  | apply extract_list_state_rel ].
+                  | apply extract_list_state_rel
+                  | apply extract_option_state_rel ].
         Qed.
 
 
@@ -753,7 +782,8 @@ Module Compilers.
             solve [ eassumption
                   | exact _
                   | apply extract_list_state_length
-                  | apply extract_list_state_rel ].
+                  | apply extract_list_state_rel
+                  | apply extract_option_state_rel ].
         Qed.
       End with_var2.
 
diff --git a/src/AbstractInterpretationZRangeProofs.v b/src/AbstractInterpretationZRangeProofs.v
index 0cafa6dda..81483714f 100644
--- a/src/AbstractInterpretationZRangeProofs.v
+++ b/src/AbstractInterpretationZRangeProofs.v
@@ -283,6 +283,7 @@ Module Compilers.
                          | simplify_ranges_t_step
                          | match goal with
                            | [ |- context[andb ?a ?b = true] ] => rewrite !Bool.andb_true_iff
+                           | [ H : context[andb ?a ?b = true] |- _ ] => rewrite !Bool.andb_true_iff
                            | [ H : FoldBool.fold_andb_map _ _ _ = true |- _ ] => rewrite FoldBool.fold_andb_map_iff in H
                            | [ |- FoldBool.fold_andb_map _ _ _ = true ] => rewrite FoldBool.fold_andb_map_iff
                            | [ H : forall (x : option _), _ |- _ ] => pose proof (H None); specialize (fun x => H (Some x))
@@ -315,7 +316,7 @@ Module Compilers.
                              => rewrite OptionList.fold_right_option_seq in H
                            | [ |- and _ _ ] => apply conj
                            end
-                         | progress cbv [bool_eq option_map List.nth_default Definitions.Z.bneg is_bounded_by_bool] in *
+                         | progress cbv [bool_eq option_map List.nth_default Definitions.Z.bneg is_bounded_by_bool zrange_beq] in *
                          | match goal with
                            | [ |- ?R (nat_rect ?P ?O ?S ?n) (nat_rect ?P' ?O' ?S' ?n) = true ]
                              => is_var n; induction n; cbn [nat_rect];
@@ -358,6 +359,9 @@ Module Compilers.
                              => apply H; clear H
                            | [ H : forall a b, ?R a b = true -> forall c d, ?R' c d = true -> forall e f, ?R'' e f = true -> ?R''' (?F _ _ _) (?G _ _ _) = true |- ?R''' (?F _ _ _) (?G _ _ _) = true ]
                              => apply H; clear H
+                           | [ H : context[ZRange.type.base.option.is_bounded_by (?f (Some _) (Some _)) (?g _ _) = true]
+                               |- ZRange.type.base.option.is_bounded_by (?f (Some _) (Some _)) (?g _ _) = true ]
+                             => apply H
                            end ].
 
           Local Lemma mul_by_halves_bounds x y n :
@@ -422,7 +426,7 @@ Module Compilers.
                  | _ => idtac
                  end.
             all: cbn [type.related_hetero ZRange.ident.option.interp ident.interp ident.gen_interp respectful_hetero type.interp ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp ZRange.type.base.option.Some ZRange.ident.option.of_literal].
-            all: cbv [respectful_hetero option_map list_case].
+            all: cbv [respectful_hetero option_map option_rect zrange_rect list_case].
             all: intros.
             all: destruct_head_hnf' prod.
             all: destruct_head_hnf' option.
@@ -497,7 +501,7 @@ Module Compilers.
                         end.
             all: try solve [ cbv [Proper respectful Basics.flip]; constructor; intros; lia ].
             all: try solve [ cbv [Proper respectful Basics.flip]; constructor; intros; autorewrite with zsimplify_const; lia ].
-            all: cbv [is_bounded_by_bool upper lower]; rewrite ?Bool.andb_true_iff, ?Z.leb_le.
+            all: cbv [is_bounded_by_bool ZRange.upper ZRange.lower]; rewrite ?Bool.andb_true_iff, ?Z.leb_le.
             all: try solve [ match goal with
                              | [ |- ((0 <= _ mod _ <= _) /\ (0 <= _ <= _))%Z ]
                                => Z.div_mod_to_quot_rem; nia
@@ -507,6 +511,7 @@ Module Compilers.
               rewrite Z.le_sub_1_iff.
               break_innermost_match; Z.ltb_to_lt;
                 auto with zarith. }
+            { non_arith_t; Z.ltb_to_lt; reflexivity. }
           Qed.
         End interp_related.
       End option.
diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v
index 1c6cec4c7..f0c161dc2 100644
--- a/src/BoundsPipeline.v
+++ b/src/BoundsPipeline.v
@@ -141,6 +141,7 @@ Module Pipeline.
            => fun 'tt 'tt => (false, nil, nil)
          | base.type.nat
          | base.type.bool
+         | base.type.zrange
            => fun _ _ => (false, nil, nil)
          | base.type.Z
            => fun a b
@@ -153,6 +154,19 @@ Module Pipeline.
                       then (false, nil, nil)
                       else (false, nil, ((a, b)::nil))
                  end
+         | base.type.option A
+           => fun a b
+              => match a, b with
+                 | None, None => (false, nil, nil)
+                 | Some _, None => (false, nil, nil)
+                 | None, Some _ => (true, nil, nil)
+                 | Some None, Some None
+                 | Some (Some _), Some None
+                 | Some None, Some (Some _)
+                   => (false, nil, nil)
+                 | Some (Some a), Some (Some b)
+                   => @find_too_loose_base_bounds A a b
+                 end
          | base.type.prod A B
            => fun '(ra, rb) '(ra', rb')
               => let '(b1, lens1, ls1) := @find_too_loose_base_bounds A ra ra' in
diff --git a/src/CStringification.v b/src/CStringification.v
index 0cdf55c99..9ae80d140 100644
--- a/src/CStringification.v
+++ b/src/CStringification.v
@@ -41,12 +41,16 @@ Module Compilers.
                | base.type.Z => @show zrange _
                | base.type.bool => @show bool _
                | base.type.nat => @show nat _
+               | base.type.zrange => @show zrange _
                | base.type.prod A B
                  => fun _ '(a, b)
                     => "(" ++ @show_interp A false a ++ ", " ++ @show_interp B true b ++ ")"
                | base.type.list A
                  => let SA := @show_interp A in
                     @show (list (ZRange.type.base.interp A)) _
+               | base.type.option A
+                 => let SA := @show_interp A in
+                    @show (option (ZRange.type.base.interp A)) _
                end%string.
           Global Existing Instance show_interp.
           Module Export option.
@@ -56,6 +60,7 @@ Module Compilers.
                  | base.type.Z => @show (option zrange) _
                  | base.type.bool => @show (option bool) _
                  | base.type.nat => @show (option nat) _
+                 | base.type.zrange => @show (option zrange) _
                  | base.type.prod A B
                    => let SA := @show_interp A in
                       let SB := @show_interp B in
@@ -63,6 +68,9 @@ Module Compilers.
                  | base.type.list A
                    => let SA := @show_interp A in
                       @show (option (list (ZRange.type.base.option.interp A))) _
+                 | base.type.option A
+                   => let SA := @show_interp A in
+                      @show (option (option (ZRange.type.base.option.interp A))) _
                  end.
             Global Existing Instance show_interp.
           End option.
@@ -90,6 +98,7 @@ Module Compilers.
                        | base.type.Z => "ℤ"
                        | base.type.bool => "𝔹"
                        | base.type.nat => "ℕ"
+                       | base.type.zrange => "zrange"
                        end.
           Fixpoint show_type (with_parens : bool) (t : base.type) : string
             := match t with
@@ -98,6 +107,10 @@ Module Compilers.
                                         with_parens
                                         (@show_type false A ++ " * " ++ @show_type true B)
                | base.type.list A => "[" ++ @show_type false A ++ "]"
+               | base.type.option A
+                 => maybe_wrap_parens
+                      with_parens
+                      ("option " ++ @show_type true A)
                end.
           Fixpoint show_base_interp {t} : Show (base.base_interp t)
             := match t with
@@ -105,6 +118,7 @@ Module Compilers.
                | base.type.Z => @show Z _
                | base.type.bool => @show bool _
                | base.type.nat => @show nat _
+               | base.type.zrange => @show zrange _
                end.
           Global Existing Instance show_base_interp.
           Fixpoint show_interp {t} : Show (base.interp t)
@@ -112,6 +126,7 @@ Module Compilers.
                | base.type.type_base t => @show (base.base_interp t) _
                | base.type.prod A B => @show (base.interp A * base.interp B) _
                | base.type.list A => @show (list (base.interp A)) _
+               | base.type.option A => @show (option (base.interp A)) _
                end.
           Global Existing Instance show_interp.
           Global Instance show : Show base.type := show_type.
@@ -174,7 +189,9 @@ Module Compilers.
                    | Some c, None => Some (c ++ ", ??")
                    | None, None => None
                    end
-           | base.type.list A => fun _ => None
+           | base.type.list _
+           | base.type.option _
+             => fun _ => None
            end.
       Fixpoint make_cast {t} : ZRange.type.option.interp t -> option string
         := match t with
@@ -212,6 +229,9 @@ Module Compilers.
              | ident.Nat_add => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 50) (x 50%nat ++ " +ℕ " ++ y 49%nat), ZRange.type.base.option.None)
              | ident.Nat_sub => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 50) (x 50%nat ++ " -ℕ " ++ y 49%nat), ZRange.type.base.option.None)
              | ident.Nat_eqb => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 70) (x 69%nat ++ " =ℕ " ++ y 69%nat), ZRange.type.base.option.None)
+             | ident.Some _
+               => fun args => (show_application with_casts (fun _ => "Some") args, ZRange.type.base.option.None)
+             | ident.None _ => fun 'tt => (fun _ => "None", ZRange.type.base.option.None)
              | ident.nil t => fun 'tt => (fun _ => "[]", ZRange.type.base.option.None)
              | ident.cons t => fun '(x, ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 60) (maybe_wrap_cast with_casts x 59%nat ++ " :: " ++ y 60%nat), ZRange.type.base.option.None)
              | ident.pair A B => fun '(x, (y, tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 201) (maybe_wrap_cast with_casts x 201%nat ++ ", " ++ maybe_wrap_cast with_casts y 200%nat), ZRange.type.base.option.None)
@@ -223,6 +243,8 @@ Module Compilers.
                => fun args => (show_application with_casts (fun _ => "nat_rect") args, ZRange.type.base.option.None)
              | ident.nat_rect_arrow P Q
                => fun args => (show_application with_casts (fun _ => "nat_rect(→)") args, ZRange.type.base.option.None)
+             | ident.option_rect A P
+               => fun args => (show_application with_casts (fun _ => "option_rect") args, ZRange.type.base.option.None)
              | ident.list_rect A P
                => fun args => (show_application with_casts (fun _ => "list_rect") args, ZRange.type.base.option.None)
              | ident.list_case A P
@@ -265,7 +287,9 @@ Module Compilers.
              | ident.Z_div => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 40) (x 40%nat ++ " / " ++ y 39%nat), ZRange.type.base.option.None)
              | ident.Z_modulo => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 40) (x 40%nat ++ " mod " ++ y 39%nat), ZRange.type.base.option.None)
              | ident.Z_eqb => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 70) (x 69%nat ++ " = " ++ y 69%nat), ZRange.type.base.option.None)
+             | ident.Z_ltb => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 70) (x 69%nat ++ " < " ++ y 69%nat), ZRange.type.base.option.None)
              | ident.Z_leb => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 70) (x 69%nat ++ " ≤ " ++ y 69%nat), ZRange.type.base.option.None)
+             | ident.Z_gtb => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 70) (x 69%nat ++ " > " ++ y 69%nat), ZRange.type.base.option.None)
              | ident.Z_geb => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 70) (x 69%nat ++ " ≥ " ++ y 69%nat), ZRange.type.base.option.None)
              | ident.Z_log2
                => fun args => (show_application with_casts (fun _ => "Z.log2") args, ZRange.type.base.option.None)
@@ -275,6 +299,10 @@ Module Compilers.
                => fun args => (show_application with_casts (fun _ => "(ℕ→ℤ)") args, ZRange.type.base.option.None)
              | ident.Z_to_nat
                => fun args => (show_application with_casts (fun _ => "(ℤ→ℕ)") args, ZRange.type.base.option.None)
+             | ident.Z_min
+               => fun args => (show_application with_casts (fun _ => "Z.min") args, ZRange.type.base.option.None)
+             | ident.Z_max
+               => fun args => (show_application with_casts (fun _ => "Z.max") args, ZRange.type.base.option.None)
              | ident.Z_shiftr => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 30) (x 30%nat ++ " >> " ++ y 29%nat), ZRange.type.base.option.None)
              | ident.Z_shiftl => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 30) (x 30%nat ++ " << " ++ y 29%nat), ZRange.type.base.option.None)
              | ident.Z_land => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 50) (x 50%nat ++ " & " ++ y 49%nat), ZRange.type.base.option.None)
@@ -303,6 +331,9 @@ Module Compilers.
                => fun '((x, xr), tt) => (x, Some range)
              | ident.Z_cast2 (r1, r2)
                => fun '((x, xr), tt) => (x, (Some r1, Some r2))
+             | ident.Build_zrange => fun '((x, xr), ((y, yr), tt)) => (fun lvl => maybe_wrap_parens (Nat.ltb lvl 0) ("r[" ++ x 60%nat ++ " ~> " ++ y 200%nat), ZRange.type.base.option.None)
+             | ident.zrange_rect A
+               => fun args => (show_application with_casts (fun _ => "zrange_rect") args, ZRange.type.base.option.None)
              | ident.fancy_add log2wordmax imm
                => fun args => (show_application with_casts (fun lvl' => maybe_wrap_parens (Nat.ltb lvl' 11) ("fancy.add 2^" ++ decimal_string_of_Z log2wordmax ++ " " ++ HexString.of_Z imm)) args, ZRange.type.base.option.None)
              | ident.fancy_addc log2wordmax imm
@@ -367,6 +398,9 @@ Module Compilers.
                 | ident.List_fold_right A B => "fold_right"
                 | ident.List_update_nth T => "update_nth"
                 | ident.List_nth_default T => "nth"
+                | ident.Some _ => "Some"
+                | ident.None _ => "None"
+                | ident.option_rect _ _ => "option_rect"
                 | ident.Z_add => "(+)"
                 | ident.Z_mul => "( * )"
                 | ident.Z_pow => "(^)"
@@ -376,7 +410,11 @@ Module Compilers.
                 | ident.Z_modulo => "(mod)"
                 | ident.Z_eqb => "(=)"
                 | ident.Z_leb => "(≤)"
+                | ident.Z_ltb => "(<)"
                 | ident.Z_geb => "(≥)"
+                | ident.Z_gtb => "(>)"
+                | ident.Z_min => "min"
+                | ident.Z_max => "max"
                 | ident.Z_log2 => "log₂"
                 | ident.Z_log2_up => "⌈log₂⌉"
                 | ident.Z_of_nat => "(ℕ→ℤ)"
@@ -399,6 +437,8 @@ Module Compilers.
                 | ident.Z_cc_m => "Z.cc_m"
                 | ident.Z_cast range => "(" ++ show_range_or_ctype range ++ ")"
                 | ident.Z_cast2 (r1, r2) => "(" ++ show_range_or_ctype r1 ++ ", " ++ show_range_or_ctype r2 ++ ")"
+                | ident.Build_zrange => "Build_zrange"
+                | ident.zrange_rect _ => "zrange_rect"
                 | ident.fancy_add log2wordmax imm
                   => maybe_wrap_parens with_parens ("fancy.add 2^" ++ decimal_string_of_Z log2wordmax ++ " " ++ HexString.of_Z imm)
                 | ident.fancy_addc log2wordmax imm
@@ -657,6 +697,7 @@ Module Compilers.
              | base.type.type_base _ => unit
              | base.type.prod A B => base_interp A * base_interp B
              | base.type.list A => list (base_interp A)
+             | base.type.option A => option (base_interp A)
              end%type.
 
         Module option.
@@ -666,6 +707,7 @@ Module Compilers.
                | base.type.type_base _ => unit
                | base.type.prod A B => interp A * interp B
                | base.type.list A => option (list (interp A))
+               | base.type.option A => option (option (interp A))
                end%type.
           Fixpoint None {t} : interp t
             := match t with
@@ -673,6 +715,7 @@ Module Compilers.
                | base.type.type_base _ => tt
                | base.type.prod A B => (@None A, @None B)
                | base.type.list A => Datatypes.None
+               | base.type.option A => Datatypes.None
                end.
           Fixpoint Some {t} : base_interp t -> interp t
             := match t with
@@ -680,6 +723,7 @@ Module Compilers.
                | base.type.type_base _ => fun tt => tt
                | base.type.prod A B => fun '(a, b) => (@Some A a, @Some B b)
                | base.type.list A => fun ls => Datatypes.Some (List.map (@Some A) ls)
+               | base.type.option A => fun ls => Datatypes.Some (Option.map (@Some A) ls)
                end.
         End option.
 
@@ -773,6 +817,8 @@ Module Compilers.
                => unit
              | base.type.nat
              | base.type.bool
+             | base.type.zrange
+             | base.type.option _
                => Empty_set
              | base.type.Z => string * option int.type
              | base.type.prod A B => base_var_data A * base_var_data B
@@ -790,6 +836,8 @@ Module Compilers.
                => unit
              | base.type.nat
              | base.type.bool
+             | base.type.zrange
+             | base.type.option _
                => Empty_set
              | base.type.Z => string
              | base.type.prod A B => base_var_names A * base_var_names B
@@ -806,6 +854,8 @@ Module Compilers.
              | base.type.unit
              | base.type.nat
              | base.type.bool
+             | base.type.zrange
+             | base.type.option _
                => fun x => x
              | base.type.Z => @fst _ _
              | base.type.prod A B
@@ -825,6 +875,7 @@ Module Compilers.
              | base.type.prod A B
                => arith_expr_for_base A * arith_expr_for_base B
              | base.type.list A => list (arith_expr_for_base A)
+             | base.type.option A => option (arith_expr_for_base A)
              | base.type.type_base _ as t
                => base.interp t
              end.
@@ -969,6 +1020,13 @@ Module Compilers.
                                         (List.combine r1 ls)
                    | None => ls
                    end
+             | base.type.option A
+               => fun r1 ls
+                 => match r1 with
+                   | Some r1 => Option.map (fun '(r, e) => @cast_down_if_needed A r e)
+                                        (Option.combine r1 ls)
+                   | None => ls
+                   end
              end.
 
         Definition Zcast_up_if_needed
@@ -997,6 +1055,13 @@ Module Compilers.
                                         (List.combine r1 ls)
                    | None => ls
                    end
+             | base.type.option A
+               => fun r1 ls
+                 => match r1 with
+                   | Some r1 => Option.map (fun '(r, e) => @cast_up_if_needed A r e)
+                                        (Option.combine r1 ls)
+                   | None => ls
+                   end
              end.
 
         Definition cast_bigger_up_if_needed
@@ -1216,6 +1281,9 @@ Module Compilers.
                | ident.bool_rect _
                | ident.nat_rect _
                | ident.nat_rect_arrow _ _
+               | ident.Some _
+               | ident.None _
+               | ident.option_rect _ _
                | ident.list_rect _ _
                | ident.list_case _ _
                | ident.List_length _
@@ -1237,7 +1305,11 @@ Module Compilers.
                | ident.Z_modulo
                | ident.Z_eqb
                | ident.Z_leb
+               | ident.Z_ltb
                | ident.Z_geb
+               | ident.Z_gtb
+               | ident.Z_min
+               | ident.Z_max
                | ident.Z_log2
                | ident.Z_log2_up
                | ident.Z_of_nat
@@ -1254,6 +1326,8 @@ Module Compilers.
                | ident.Z_cc_m
                | ident.Z_cast _
                | ident.Z_cast2 _
+               | ident.Build_zrange
+               | ident.zrange_rect _
                | ident.fancy_add _ _
                | ident.fancy_addc _ _
                | ident.fancy_sub _ _
@@ -1369,6 +1443,7 @@ Module Compilers.
                             (fun i => (List_nth i @@ Var type.Zptr n, r))%core%Cexpr
                             (List.seq 0 len))
                | base.type.list _
+               | base.type.option _
                | base.type.type_base _
                  => fun _ _ => inr ["Invalid type " ++ show false t]%string
                end.
@@ -1438,7 +1513,9 @@ Module Compilers.
                         ret (List.map
                                (fun '(i, (e, _)) => AssignNth n i e)
                                (List.combine (List.seq 0 len) ls)))
-               | base.type.list _ => fun _ _ => inr ["Invalid type of expr: " ++ show false t]%string
+               | base.type.list _
+               | base.type.option _
+                 => fun _ _ => inr ["Invalid type of expr: " ++ show false t]%string
                end%list.
           Definition make_return_assignment_of_arith {t}
             : var_data t
@@ -1537,11 +1614,12 @@ Module Compilers.
                             fun retptr => [Call (Z_mul_split s @@ (retptr, (e1, e2)))%Cexpr]))
                | Some s, ident.Z_add_get_carry as idc
                | Some s, ident.Z_sub_get_borrow as idc
-                 => let idc' : ident _ _ := invert_Some match idc with
-                                                       | ident.Z_add_get_carry => Some (Z_add_with_get_carry s)
-                                                       | ident.Z_sub_get_borrow => Some (Z_sub_with_get_borrow s)
-                                                       | _ => None
-                                                       end in
+                 => let idc' : ident _ _ := Option.invert_Some
+                                              match idc with
+                                              | ident.Z_add_get_carry => Some (Z_add_with_get_carry s)
+                                              | ident.Z_sub_get_borrow => Some (Z_sub_with_get_borrow s)
+                                              | _ => None
+                                              end in
                    (_ ,, _ ,, _ ,, _
                       <- bounds_check do_bounds_check "first argument to" idc s e1v r1,
                     bounds_check do_bounds_check "second argument to" idc s e2v r2,
@@ -1566,11 +1644,12 @@ Module Compilers.
                with
                | Some s, ident.Z_add_with_get_carry as idc
                | Some s, ident.Z_sub_with_get_borrow as idc
-                 => let idc' : ident _ _ := invert_Some match idc with
-                                                       | ident.Z_add_with_get_carry => Some (Z_add_with_get_carry s)
-                                                       | ident.Z_sub_with_get_borrow => Some (Z_sub_with_get_borrow s)
-                                                       | _ => None
-                                                       end in
+                 => let idc' : ident _ _ := Option.invert_Some
+                                              match idc with
+                                              | ident.Z_add_with_get_carry => Some (Z_add_with_get_carry s)
+                                              | ident.Z_sub_with_get_borrow => Some (Z_sub_with_get_borrow s)
+                                              | _ => None
+                                              end in
                    (_ ,, _ ,, _ ,, _ ,, _
                       <- (bounds_check do_bounds_check "first (carry) argument to" idc 1 e1v r1,
                          bounds_check do_bounds_check "second argument to" idc s e2v r2,
@@ -1691,6 +1770,7 @@ Module Compilers.
                | base.type.type_base t => 1
                | base.type.prod A B => size_of_type A + size_of_type B
                | base.type.list A => 1
+               | base.type.option A => 1
                end%positive.
 
           Let make_uniform_assign_expr_of_PHOAS
@@ -1779,6 +1859,7 @@ Module Compilers.
                | base.type.unit
                  => fun _ => Some (count, tt)
                | base.type.list _
+               | base.type.option _
                | base.type.type_base _
                  => fun _ => None
                end%option.
@@ -2113,9 +2194,11 @@ Module Compilers.
            | base.type.list base.type.Z
              => fun '(n, r, len) => ["const " ++ String.type.primitive.to_string prefix type.Z r ++ " " ++ n ++ "[" ++ decimal_string_of_Z (Z.of_nat len) ++ "]"]
            | base.type.list _ => fun _ => ["#error ""complex list"";"]
+           | base.type.option _ => fun _ => ["#error option;"]
            | base.type.unit => fun _ => ["#error unit;"]
            | base.type.nat => fun _ => ["#error ℕ;"]
            | base.type.bool => fun _ => ["#error bool;"]
+           | base.type.zrange => fun _ => ["#error zrange;"]
            end.
 
       Definition to_arg_list (prefix : string) {t} : var_data t -> list string
@@ -2141,9 +2224,11 @@ Module Compilers.
            | base.type.list base.type.Z
              => fun '(n, r, len) => [String.type.primitive.to_string prefix type.Z r ++ " " ++ n ++ "[" ++ decimal_string_of_Z (Z.of_nat len) ++ "]"]
            | base.type.list _ => fun _ => ["#error ""complex list"";"]
+           | base.type.option _ => fun _ => ["#error option;"]
            | base.type.unit => fun _ => ["#error unit;"]
            | base.type.nat => fun _ => ["#error ℕ;"]
            | base.type.bool => fun _ => ["#error bool;"]
+           | base.type.zrange => fun _ => ["#error zrange;"]
            end.
 
       Definition to_retarg_list (prefix : string) {t} : var_data t -> list string
@@ -2171,9 +2256,11 @@ Module Compilers.
                          | Some arg => show false arg
                          | None => show false arg
                          end]%string
+           | base.type.option _
            | base.type.unit
            | base.type.bool
            | base.type.nat
+           | base.type.zrange
              => fun _ _ => nil
            end%list.
 
diff --git a/src/CompilersTestCases.v b/src/CompilersTestCases.v
index c02b4e2fc..d5c8b2579 100644
--- a/src/CompilersTestCases.v
+++ b/src/CompilersTestCases.v
@@ -61,7 +61,7 @@ Module testrewrite.
                                       (RewriteRules.RewriteNBE (fun var =>
                 (\z , ((\ x , expr_let y := ##5 in $y + ($z + (#ident.fst @ $x + #ident.snd @ $x)))
                          @ (##1, ##7)))%expr) _)
-                (Some r[0~>100]%zrange, tt).
+                (Datatypes.Some r[0~>100]%zrange, tt).
 End testrewrite.
 Module testpartial.
   Import expr.
@@ -85,7 +85,7 @@ Module testpartial.
                 partial.default_relax_zrange
                 (\z , ((\ x , expr_let y := ##5 in $y + ($z + (#ident.fst @ $x + #ident.snd @ $x)))
                          @ (##1, ##7)))%expr
-                (Some r[0~>100]%zrange, tt).
+                (Datatypes.Some r[0~>100]%zrange, tt).
 End testpartial.
 
 Module test2.
diff --git a/src/GENERATEDIdentifiersWithoutTypes.v b/src/GENERATEDIdentifiersWithoutTypes.v
index a5e96870f..d2651f53b 100644
--- a/src/GENERATEDIdentifiersWithoutTypes.v
+++ b/src/GENERATEDIdentifiersWithoutTypes.v
@@ -23,7 +23,7 @@ Module Compilers.
     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).
+        Inductive type := var (p : positive) | type_base (t : Compilers.base.type.base) | prod (A B : type) | list (A : type) | option (A : type).
       End type.
       Notation type := type.type.
 
@@ -32,18 +32,20 @@ Module Compilers.
            | 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)
+           | Compilers.base.type.option A => type.option (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
+                           | Datatypes.Some t => t
+                           | Datatypes.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)
+           | type.option A => Compilers.base.type.option (subst_default A evar_map)
            end.
 
       Fixpoint collect_vars (t : type) : PositiveSet.t
@@ -52,6 +54,7 @@ Module Compilers.
            | type.type_base t => PositiveSet.empty
            | type.prod A B => PositiveSet.union (collect_vars A) (collect_vars B)
            | type.list A => collect_vars A
+           | type.option A => collect_vars A
            end.
 
       Module Notations.
@@ -435,6 +438,13 @@ print_ident = r"""Inductive ident : defaults.type -> Set :=
                  (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_ltb : 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) ->
@@ -442,6 +452,13 @@ print_ident = r"""Inductive ident : defaults.type -> Set :=
                  (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_gtb : 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) ->
@@ -480,6 +497,20 @@ print_ident = r"""Inductive ident : defaults.type -> Set :=
                  (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_min : 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_max : 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) ->
@@ -605,6 +636,41 @@ print_ident = r"""Inductive ident : defaults.type -> Set :=
                  (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
+  | option_Some : 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.option A))%ptype
+  | option_None : forall A : Compilers.base.type,
+                  ident
+                    ((fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.option A))
+  | option_rect : forall A P : Compilers.base.type,
+                  ident
+                    (((fun x : Compilers.base.type => type.base x) A ->
+                      (fun x : Compilers.base.type => type.base x) P) ->
+                     ((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.option A) ->
+                     (fun x : Compilers.base.type => type.base x) P)%ptype
+  | Build_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) ->
+                      (fun x : Compilers.base.type => type.base x)
+                        (Compilers.base.type.type_base base.type.zrange))%ptype
+  | zrange_rect : forall P : Compilers.base.type,
+                  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) P) ->
+                     (fun x : Compilers.base.type => type.base x)
+                       (Compilers.base.type.type_base base.type.zrange) ->
+                     (fun x : Compilers.base.type => type.base x) P)%ptype
   | fancy_add : Z ->
                 Z ->
                 ident
@@ -755,13 +821,17 @@ show_match_ident = r"""match # with
  | ident.Z_log2_up =>
  | ident.Z_eqb =>
  | ident.Z_leb =>
+ | ident.Z_ltb =>
  | ident.Z_geb =>
+ | ident.Z_gtb =>
  | ident.Z_of_nat =>
  | ident.Z_to_nat =>
  | ident.Z_shiftr =>
  | ident.Z_shiftl =>
  | ident.Z_land =>
  | ident.Z_lor =>
+ | ident.Z_min =>
+ | ident.Z_max =>
  | ident.Z_bneg =>
  | ident.Z_lnot_modulo =>
  | ident.Z_mul_split =>
@@ -776,6 +846,11 @@ show_match_ident = r"""match # with
  | ident.Z_cc_m =>
  | ident.Z_cast range =>
  | ident.Z_cast2 range =>
+ | ident.option_Some A =>
+ | ident.option_None A =>
+ | ident.option_rect A P =>
+ | ident.Build_zrange =>
+ | ident.zrange_rect P =>
  | ident.fancy_add log2wordmax imm =>
  | ident.fancy_addc log2wordmax imm =>
  | ident.fancy_sub log2wordmax imm =>
@@ -804,7 +879,7 @@ indent0 = '    '
 indent1 = '  ' + indent0
 indent2 = '  ' + indent1
 #exts = ('Unit', 'Z', 'Bool', 'Nat')
-base_types = [('%sbase.type.' % prefix) + i for i in ('unit', 'Z', 'bool', 'nat')]
+base_types = [('%sbase.type.' % prefix) + i for i in ('unit', 'Z', 'bool', 'nat', 'zrange')]
 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')
@@ -862,7 +937,7 @@ Module Compilers.
     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).
+        Inductive type := var (p : positive) | type_base (t : Compilers.base.type.base) | prod (A B : type) | list (A : type) | option (A : type).
       End type.
       Notation type := type.type.
 
@@ -871,18 +946,20 @@ Module Compilers.
            | 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)
+           | Compilers.base.type.option A => type.option (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
+                           | Datatypes.Some t => t
+                           | Datatypes.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)
+           | type.option A => Compilers.base.type.option (subst_default A evar_map)
            end.
 
       Fixpoint collect_vars (t : type) : PositiveSet.t
@@ -891,6 +968,7 @@ Module Compilers.
            | type.type_base t => PositiveSet.empty
            | type.prod A B => PositiveSet.union (collect_vars A) (collect_vars B)
            | type.list A => collect_vars A
+           | type.option A => collect_vars A
            end.
 
       Module Notations.
@@ -1050,14 +1128,14 @@ retcode += addnewline((r"""%sDefinition is_simple (idc : ident) : bool
        '\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
+retcode += addnewline((r"""%sDefinition invert_bind_args {t} (idc : %sident.ident t) (pidc : ident) : Datatypes.option (full_types pidc)
+  := match pidc, idc return Datatypes.option (full_types pidc) with
      | %s
      | %s
-       => None
+       => Datatypes.None
      end%%cps.
 """ % (indent2, prefix,
-       '\n     | '.join(pctor + ', ' + ' '.join(ctor) + ' => Some ' + make_pair_of_types(named_ttype, ctype, ctor)
+       '\n     | '.join(pctor + ', ' + ' '.join(ctor) + ' => Datatypes.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))
 
@@ -1149,18 +1227,18 @@ retcode += addnewline((r"""%sDefinition to_typed {t} (idc : ident t) (evm : Evar
 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
+retcode += addnewline((r"""%sDefinition unify {t t'} (pidc : ident t) (idc : %sident.ident t') : Datatypes.option (type_of_list (@arg_types t pidc))
+  := match pidc, idc return Datatypes.option (type_of_list (arg_types pidc)) with
      | %s
      | %s
      | %s
-       => None
+       => Datatypes.None
      end%%cps.
 """ % (indent1, prefix,
-       '\n     | '.join('@' + pctor + ' ' + ty + ', ' + ' '.join([ctor[0], ty] + ctor[2:]) + ' => Some ' + fold_right_pair(ctor[-len(ctype):])
+       '\n     | '.join('@' + pctor + ' ' + ty + ', ' + ' '.join([ctor[0], ty] + ctor[2:]) + ' => Datatypes.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):]]))
+       '\n     | '.join('@' + pctor + ', ' + ' '.join([ctor[0]] + [i + "'" for i in ctor[1:]]) + ' => Datatypes.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))
 
@@ -1178,8 +1256,8 @@ retcode += addnewline((r"""%sDefinition of_typed_ident {t} (idc : %sident.ident
 """ % (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
+#retcode += addnewline((r"""%sDefinition retype_ident {t} (idc : %sident.ident t) : match arg_types (of_typed_ident idc) return %s with Datatypes.Some t => t | Datatypes.None => unit end -> %sident.ident t
+#  := match idc in %sident.ident t return match arg_types (of_typed_ident idc) return %s with Datatypes.Some t => t | Datatypes.None => unit end -> %sident.ident t with
 #     | %s
 #     end.
 #""" % (indent1, prefix, type_or_set, prefix, prefix, type_or_set, prefix,
@@ -1188,7 +1266,7 @@ retcode += addnewline((r"""%sDefinition of_typed_ident {t} (idc : %sident.ident
 #                        + '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 -> _'
+#                            + ('match arg_types (of_typed_ident %s) return %s with Datatypes.Some t => t | Datatypes.None => unit end -> _'
 #                               % (('%s' if ' ' not in ' '.join(ctor) else '(@%s)') % ' '.join(ctor),
 #                                  type_or_set))
 #                            + ' (* COQBUG(https://github.com/coq/coq/issues/7726) *)'))
@@ -1197,20 +1275,20 @@ retcode += addnewline((r"""%sDefinition of_typed_ident {t} (idc : %sident.ident
 
 
 
-#retcode += addnewline((r"""%sDefinition try_make_transport_ident_cps (P : ident -> Type) (idc1 idc2 : ident) : ~> option (P idc1 -> P idc2)
+#retcode += addnewline((r"""%sDefinition try_make_transport_ident_cps (P : ident -> Type) (idc1 idc2 : ident) : ~> Datatypes.option (P idc1 -> P idc2)
 #  := match idc1, idc2 with
 #     | %s
-#       => fun T k => k (Some (fun v => v))
+#       => fun T k => k (Datatypes.Some (fun v => v))
 #     | %s
-#       => fun T k => k None
+#       => fun T k => k Datatypes.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)
+#retcode += addnewline((r"""%sDefinition eta_all_option_cps {T} (f : ident -> Datatypes.option T)
+#  : Datatypes.option (ident -> T)
 #  := (%s;
-#      Some (fun c
+#      Datatypes.Some (fun c
 #            => match c with
 #               | %s
 #               end))%%option.
@@ -1326,13 +1404,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
         | Z_log2_up
         | Z_eqb
         | Z_leb
+        | Z_ltb
         | Z_geb
+        | Z_gtb
         | Z_of_nat
         | Z_to_nat
         | Z_shiftr
         | Z_shiftl
         | Z_land
         | Z_lor
+        | Z_min
+        | Z_max
         | Z_bneg
         | Z_lnot_modulo
         | Z_mul_split
@@ -1347,6 +1429,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
         | Z_cc_m
         | Z_cast
         | Z_cast2
+        | option_Some
+        | option_None
+        | option_rect
+        | Build_zrange
+        | zrange_rect
         | fancy_add
         | fancy_addc
         | fancy_sub
@@ -1407,13 +1494,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | Z_log2_up => unit
              | Z_eqb => unit
              | Z_leb => unit
+             | Z_ltb => unit
              | Z_geb => unit
+             | Z_gtb => unit
              | Z_of_nat => unit
              | Z_to_nat => unit
              | Z_shiftr => unit
              | Z_shiftl => unit
              | Z_land => unit
              | Z_lor => unit
+             | Z_min => unit
+             | Z_max => unit
              | Z_bneg => unit
              | Z_lnot_modulo => unit
              | Z_mul_split => unit
@@ -1428,6 +1519,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | Z_cc_m => unit
              | Z_cast => zrange
              | Z_cast2 => zrange * zrange
+             | option_Some => Compilers.base.type
+             | option_None => Compilers.base.type
+             | option_rect => Compilers.base.type * Compilers.base.type
+             | Build_zrange => unit
+             | zrange_rect => Compilers.base.type
              | fancy_add => Z * Z
              | fancy_addc => Z * Z
              | fancy_sub => Z * Z
@@ -1489,13 +1585,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | Z_log2_up => true
              | Z_eqb => true
              | Z_leb => true
+             | Z_ltb => true
              | Z_geb => true
+             | Z_gtb => true
              | Z_of_nat => true
              | Z_to_nat => true
              | Z_shiftr => true
              | Z_shiftl => true
              | Z_land => true
              | Z_lor => true
+             | Z_min => true
+             | Z_max => true
              | Z_bneg => true
              | Z_lnot_modulo => true
              | Z_mul_split => true
@@ -1510,6 +1610,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | Z_cc_m => true
              | Z_cast => true
              | Z_cast2 => true
+             | option_Some => false
+             | option_None => false
+             | option_rect => false
+             | Build_zrange => true
+             | zrange_rect => false
              | fancy_add => true
              | fancy_addc => true
              | fancy_sub => true
@@ -1525,86 +1630,95 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | 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
-             | Nat_eqb, Compilers.ident.Nat_eqb => 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
+        Definition invert_bind_args {t} (idc : Compilers.ident.ident t) (pidc : ident) : Datatypes.option (full_types pidc)
+          := match pidc, idc return Datatypes.option (full_types pidc) with
+             | Literal, Compilers.ident.Literal t v => Datatypes.Some (existT _ t v)
+             | Nat_succ, Compilers.ident.Nat_succ => Datatypes.Some tt
+             | Nat_pred, Compilers.ident.Nat_pred => Datatypes.Some tt
+             | Nat_max, Compilers.ident.Nat_max => Datatypes.Some tt
+             | Nat_mul, Compilers.ident.Nat_mul => Datatypes.Some tt
+             | Nat_add, Compilers.ident.Nat_add => Datatypes.Some tt
+             | Nat_sub, Compilers.ident.Nat_sub => Datatypes.Some tt
+             | Nat_eqb, Compilers.ident.Nat_eqb => Datatypes.Some tt
+             | nil, Compilers.ident.nil t => Datatypes.Some t
+             | cons, Compilers.ident.cons t => Datatypes.Some t
+             | pair, Compilers.ident.pair A B => Datatypes.Some (A, B)
+             | fst, Compilers.ident.fst A B => Datatypes.Some (A, B)
+             | snd, Compilers.ident.snd A B => Datatypes.Some (A, B)
+             | prod_rect, Compilers.ident.prod_rect A B T => Datatypes.Some (A, B, T)
+             | bool_rect, Compilers.ident.bool_rect T => Datatypes.Some T
+             | nat_rect, Compilers.ident.nat_rect P => Datatypes.Some P
+             | nat_rect_arrow, Compilers.ident.nat_rect_arrow P Q => Datatypes.Some (P, Q)
+             | list_rect, Compilers.ident.list_rect A P => Datatypes.Some (A, P)
+             | list_case, Compilers.ident.list_case A P => Datatypes.Some (A, P)
+             | List_length, Compilers.ident.List_length T => Datatypes.Some T
+             | List_seq, Compilers.ident.List_seq => Datatypes.Some tt
+             | List_firstn, Compilers.ident.List_firstn A => Datatypes.Some A
+             | List_skipn, Compilers.ident.List_skipn A => Datatypes.Some A
+             | List_repeat, Compilers.ident.List_repeat A => Datatypes.Some A
+             | List_combine, Compilers.ident.List_combine A B => Datatypes.Some (A, B)
+             | List_map, Compilers.ident.List_map A B => Datatypes.Some (A, B)
+             | List_app, Compilers.ident.List_app A => Datatypes.Some A
+             | List_rev, Compilers.ident.List_rev A => Datatypes.Some A
+             | List_flat_map, Compilers.ident.List_flat_map A B => Datatypes.Some (A, B)
+             | List_partition, Compilers.ident.List_partition A => Datatypes.Some A
+             | List_fold_right, Compilers.ident.List_fold_right A B => Datatypes.Some (A, B)
+             | List_update_nth, Compilers.ident.List_update_nth T => Datatypes.Some T
+             | List_nth_default, Compilers.ident.List_nth_default T => Datatypes.Some T
+             | Z_add, Compilers.ident.Z_add => Datatypes.Some tt
+             | Z_mul, Compilers.ident.Z_mul => Datatypes.Some tt
+             | Z_pow, Compilers.ident.Z_pow => Datatypes.Some tt
+             | Z_sub, Compilers.ident.Z_sub => Datatypes.Some tt
+             | Z_opp, Compilers.ident.Z_opp => Datatypes.Some tt
+             | Z_div, Compilers.ident.Z_div => Datatypes.Some tt
+             | Z_modulo, Compilers.ident.Z_modulo => Datatypes.Some tt
+             | Z_log2, Compilers.ident.Z_log2 => Datatypes.Some tt
+             | Z_log2_up, Compilers.ident.Z_log2_up => Datatypes.Some tt
+             | Z_eqb, Compilers.ident.Z_eqb => Datatypes.Some tt
+             | Z_leb, Compilers.ident.Z_leb => Datatypes.Some tt
+             | Z_ltb, Compilers.ident.Z_ltb => Datatypes.Some tt
+             | Z_geb, Compilers.ident.Z_geb => Datatypes.Some tt
+             | Z_gtb, Compilers.ident.Z_gtb => Datatypes.Some tt
+             | Z_of_nat, Compilers.ident.Z_of_nat => Datatypes.Some tt
+             | Z_to_nat, Compilers.ident.Z_to_nat => Datatypes.Some tt
+             | Z_shiftr, Compilers.ident.Z_shiftr => Datatypes.Some tt
+             | Z_shiftl, Compilers.ident.Z_shiftl => Datatypes.Some tt
+             | Z_land, Compilers.ident.Z_land => Datatypes.Some tt
+             | Z_lor, Compilers.ident.Z_lor => Datatypes.Some tt
+             | Z_min, Compilers.ident.Z_min => Datatypes.Some tt
+             | Z_max, Compilers.ident.Z_max => Datatypes.Some tt
+             | Z_bneg, Compilers.ident.Z_bneg => Datatypes.Some tt
+             | Z_lnot_modulo, Compilers.ident.Z_lnot_modulo => Datatypes.Some tt
+             | Z_mul_split, Compilers.ident.Z_mul_split => Datatypes.Some tt
+             | Z_add_get_carry, Compilers.ident.Z_add_get_carry => Datatypes.Some tt
+             | Z_add_with_carry, Compilers.ident.Z_add_with_carry => Datatypes.Some tt
+             | Z_add_with_get_carry, Compilers.ident.Z_add_with_get_carry => Datatypes.Some tt
+             | Z_sub_get_borrow, Compilers.ident.Z_sub_get_borrow => Datatypes.Some tt
+             | Z_sub_with_get_borrow, Compilers.ident.Z_sub_with_get_borrow => Datatypes.Some tt
+             | Z_zselect, Compilers.ident.Z_zselect => Datatypes.Some tt
+             | Z_add_modulo, Compilers.ident.Z_add_modulo => Datatypes.Some tt
+             | Z_rshi, Compilers.ident.Z_rshi => Datatypes.Some tt
+             | Z_cc_m, Compilers.ident.Z_cc_m => Datatypes.Some tt
+             | Z_cast, Compilers.ident.Z_cast range => Datatypes.Some range
+             | Z_cast2, Compilers.ident.Z_cast2 range => Datatypes.Some range
+             | option_Some, Compilers.ident.option_Some A => Datatypes.Some A
+             | option_None, Compilers.ident.option_None A => Datatypes.Some A
+             | option_rect, Compilers.ident.option_rect A P => Datatypes.Some (A, P)
+             | Build_zrange, Compilers.ident.Build_zrange => Datatypes.Some tt
+             | zrange_rect, Compilers.ident.zrange_rect P => Datatypes.Some P
+             | fancy_add, Compilers.ident.fancy_add log2wordmax imm => Datatypes.Some (log2wordmax, imm)
+             | fancy_addc, Compilers.ident.fancy_addc log2wordmax imm => Datatypes.Some (log2wordmax, imm)
+             | fancy_sub, Compilers.ident.fancy_sub log2wordmax imm => Datatypes.Some (log2wordmax, imm)
+             | fancy_subb, Compilers.ident.fancy_subb log2wordmax imm => Datatypes.Some (log2wordmax, imm)
+             | fancy_mulll, Compilers.ident.fancy_mulll log2wordmax => Datatypes.Some log2wordmax
+             | fancy_mullh, Compilers.ident.fancy_mullh log2wordmax => Datatypes.Some log2wordmax
+             | fancy_mulhl, Compilers.ident.fancy_mulhl log2wordmax => Datatypes.Some log2wordmax
+             | fancy_mulhh, Compilers.ident.fancy_mulhh log2wordmax => Datatypes.Some log2wordmax
+             | fancy_rshi, Compilers.ident.fancy_rshi log2wordmax x => Datatypes.Some (log2wordmax, x)
+             | fancy_selc, Compilers.ident.fancy_selc => Datatypes.Some tt
+             | fancy_selm, Compilers.ident.fancy_selm log2wordmax => Datatypes.Some log2wordmax
+             | fancy_sell, Compilers.ident.fancy_sell => Datatypes.Some tt
+             | fancy_addm, Compilers.ident.fancy_addm => Datatypes.Some tt
              | Literal, _
              | Nat_succ, _
              | Nat_pred, _
@@ -1649,13 +1763,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | Z_log2_up, _
              | Z_eqb, _
              | Z_leb, _
+             | Z_ltb, _
              | Z_geb, _
+             | Z_gtb, _
              | Z_of_nat, _
              | Z_to_nat, _
              | Z_shiftr, _
              | Z_shiftl, _
              | Z_land, _
              | Z_lor, _
+             | Z_min, _
+             | Z_max, _
              | Z_bneg, _
              | Z_lnot_modulo, _
              | Z_mul_split, _
@@ -1670,6 +1788,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | Z_cc_m, _
              | Z_cast, _
              | Z_cast2, _
+             | option_Some, _
+             | option_None, _
+             | option_rect, _
+             | Build_zrange, _
+             | zrange_rect, _
              | fancy_add, _
              | fancy_addc, _
              | fancy_sub, _
@@ -1683,7 +1806,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | fancy_selm, _
              | fancy_sell, _
              | fancy_addm, _
-               => None
+               => Datatypes.None
              end%cps.
 
         Definition type_of (pidc : ident) : full_types pidc -> Compilers.type Compilers.base.type
@@ -1732,13 +1855,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | 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_ltb => 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_gtb => 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_min => 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_max => 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
@@ -1753,6 +1880,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | 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
+             | option_Some => fun A => (type.base A -> type.base (Compilers.base.type.option A))%ptype
+             | option_None => fun A => (type.base (Compilers.base.type.option A))
+             | option_rect => fun arg => let '(A, P) := eta2 arg in ((type.base A -> type.base P) -> (type.base ()%etype -> type.base P) -> type.base (Compilers.base.type.option A) -> type.base P)%ptype
+             | Build_zrange => 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.zrange))%ptype
+             | zrange_rect => fun P => ((type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base P) -> type.base (Compilers.base.type.type_base base.type.zrange) -> type.base P)%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
@@ -1814,13 +1946,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | Z_log2_up => fun _ => @Compilers.ident.Z_log2_up
              | Z_eqb => fun _ => @Compilers.ident.Z_eqb
              | Z_leb => fun _ => @Compilers.ident.Z_leb
+             | Z_ltb => fun _ => @Compilers.ident.Z_ltb
              | Z_geb => fun _ => @Compilers.ident.Z_geb
+             | Z_gtb => fun _ => @Compilers.ident.Z_gtb
              | 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_min => fun _ => @Compilers.ident.Z_min
+             | Z_max => fun _ => @Compilers.ident.Z_max
              | 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
@@ -1835,6 +1971,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | 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
+             | option_Some => fun A => @Compilers.ident.option_Some A
+             | option_None => fun A => @Compilers.ident.option_None A
+             | option_rect => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of option_rect arg') with (A, P) => @Compilers.ident.option_rect A P end
+             | Build_zrange => fun _ => @Compilers.ident.Build_zrange
+             | zrange_rect => fun P => @Compilers.ident.zrange_rect P
              | 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
@@ -1903,13 +2044,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | 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_ltb => f _ Compilers.ident.Z_ltb
            | Compilers.ident.Z_geb => f _ Compilers.ident.Z_geb
+           | Compilers.ident.Z_gtb => f _ Compilers.ident.Z_gtb
            | 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_min => f _ Compilers.ident.Z_min
+           | Compilers.ident.Z_max => f _ Compilers.ident.Z_max
            | 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
@@ -1924,6 +2069,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | 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.option_Some A => f _ (@Compilers.ident.option_Some A)
+           | Compilers.ident.option_None A => f _ (@Compilers.ident.option_None A)
+           | Compilers.ident.option_rect A P => f _ (@Compilers.ident.option_rect A P)
+           | Compilers.ident.Build_zrange => f _ Compilers.ident.Build_zrange
+           | Compilers.ident.zrange_rect P => f _ (@Compilers.ident.zrange_rect P)
            | 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)
@@ -1984,13 +2134,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
       | 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_ltb : 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_gtb : 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_min : 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_max : 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
@@ -2005,6 +2159,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
       | 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
+      | option_Some {A : base.type} : ident (type.base A -> type.base (base.type.option A))%ptype
+      | option_None {A : base.type} : ident (type.base (base.type.option A))
+      | option_rect {A : base.type} {P : base.type} : ident ((type.base A -> type.base P) -> (type.base ()%pbtype -> type.base P) -> type.base (base.type.option A) -> type.base P)%ptype
+      | Build_zrange : 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.zrange))%ptype
+      | zrange_rect {P : base.type} : ident ((type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base P) -> type.base (base.type.type_base base.type.zrange) -> type.base P)%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
@@ -2065,13 +2224,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @Z_log2_up => Raw.ident.Z_log2_up
            | @Z_eqb => Raw.ident.Z_eqb
            | @Z_leb => Raw.ident.Z_leb
+           | @Z_ltb => Raw.ident.Z_ltb
            | @Z_geb => Raw.ident.Z_geb
+           | @Z_gtb => Raw.ident.Z_gtb
            | @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_min => Raw.ident.Z_min
+           | @Z_max => Raw.ident.Z_max
            | @Z_bneg => Raw.ident.Z_bneg
            | @Z_lnot_modulo => Raw.ident.Z_lnot_modulo
            | @Z_mul_split => Raw.ident.Z_mul_split
@@ -2086,6 +2249,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @Z_cc_m => Raw.ident.Z_cc_m
            | @Z_cast => Raw.ident.Z_cast
            | @Z_cast2 => Raw.ident.Z_cast2
+           | @option_Some A => Raw.ident.option_Some
+           | @option_None A => Raw.ident.option_None
+           | @option_rect A P => Raw.ident.option_rect
+           | @Build_zrange => Raw.ident.Build_zrange
+           | @zrange_rect P => Raw.ident.zrange_rect
            | @fancy_add => Raw.ident.fancy_add
            | @fancy_addc => Raw.ident.fancy_addc
            | @fancy_sub => Raw.ident.fancy_sub
@@ -2147,13 +2315,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @Z_log2_up => []
            | @Z_eqb => []
            | @Z_leb => []
+           | @Z_ltb => []
            | @Z_geb => []
+           | @Z_gtb => []
            | @Z_of_nat => []
            | @Z_to_nat => []
            | @Z_shiftr => []
            | @Z_shiftl => []
            | @Z_land => []
            | @Z_lor => []
+           | @Z_min => []
+           | @Z_max => []
            | @Z_bneg => []
            | @Z_lnot_modulo => []
            | @Z_mul_split => []
@@ -2168,6 +2340,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @Z_cc_m => []
            | @Z_cast => [zrange : Type]
            | @Z_cast2 => [zrange * zrange : Type]
+           | @option_Some A => []
+           | @option_None A => []
+           | @option_rect A P => []
+           | @Build_zrange => []
+           | @zrange_rect P => []
            | @fancy_add => [Z : Type; Z : Type]
            | @fancy_addc => [Z : Type; Z : Type]
            | @fancy_sub => [Z : Type; Z : Type]
@@ -2229,13 +2406,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @Z_log2_up => fun _ => @Compilers.ident.Z_log2_up
            | @Z_eqb => fun _ => @Compilers.ident.Z_eqb
            | @Z_leb => fun _ => @Compilers.ident.Z_leb
+           | @Z_ltb => fun _ => @Compilers.ident.Z_ltb
            | @Z_geb => fun _ => @Compilers.ident.Z_geb
+           | @Z_gtb => fun _ => @Compilers.ident.Z_gtb
            | @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_min => fun _ => @Compilers.ident.Z_min
+           | @Z_max => fun _ => @Compilers.ident.Z_max
            | @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
@@ -2250,6 +2431,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @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
+           | @option_Some A => fun _ => @Compilers.ident.option_Some _
+           | @option_None A => fun _ => @Compilers.ident.option_None _
+           | @option_rect A P => fun _ => @Compilers.ident.option_rect _ _
+           | @Build_zrange => fun _ => @Compilers.ident.Build_zrange
+           | @zrange_rect P => fun _ => @Compilers.ident.zrange_rect _
            | @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
@@ -2265,89 +2451,99 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @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
-           | @Nat_eqb, Compilers.ident.Nat_eqb => 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
+      Definition unify {t t'} (pidc : ident t) (idc : Compilers.ident.ident t') : Datatypes.option (type_of_list (@arg_types t pidc))
+        := match pidc, idc return Datatypes.option (type_of_list (arg_types pidc)) with
+           | @Literal Compilers.base.type.unit, Compilers.ident.Literal Compilers.base.type.unit v => Datatypes.Some (v, tt)
+           | @Literal Compilers.base.type.Z, Compilers.ident.Literal Compilers.base.type.Z v => Datatypes.Some (v, tt)
+           | @Literal Compilers.base.type.bool, Compilers.ident.Literal Compilers.base.type.bool v => Datatypes.Some (v, tt)
+           | @Literal Compilers.base.type.nat, Compilers.ident.Literal Compilers.base.type.nat v => Datatypes.Some (v, tt)
+           | @Literal Compilers.base.type.zrange, Compilers.ident.Literal Compilers.base.type.zrange v => Datatypes.Some (v, tt)
+           | @Nat_succ, Compilers.ident.Nat_succ => Datatypes.Some tt
+           | @Nat_pred, Compilers.ident.Nat_pred => Datatypes.Some tt
+           | @Nat_max, Compilers.ident.Nat_max => Datatypes.Some tt
+           | @Nat_mul, Compilers.ident.Nat_mul => Datatypes.Some tt
+           | @Nat_add, Compilers.ident.Nat_add => Datatypes.Some tt
+           | @Nat_sub, Compilers.ident.Nat_sub => Datatypes.Some tt
+           | @Nat_eqb, Compilers.ident.Nat_eqb => Datatypes.Some tt
+           | @nil t, Compilers.ident.nil t' => Datatypes.Some tt
+           | @cons t, Compilers.ident.cons t' => Datatypes.Some tt
+           | @pair A B, Compilers.ident.pair A' B' => Datatypes.Some tt
+           | @fst A B, Compilers.ident.fst A' B' => Datatypes.Some tt
+           | @snd A B, Compilers.ident.snd A' B' => Datatypes.Some tt
+           | @prod_rect A B T, Compilers.ident.prod_rect A' B' T' => Datatypes.Some tt
+           | @bool_rect T, Compilers.ident.bool_rect T' => Datatypes.Some tt
+           | @nat_rect P, Compilers.ident.nat_rect P' => Datatypes.Some tt
+           | @nat_rect_arrow P Q, Compilers.ident.nat_rect_arrow P' Q' => Datatypes.Some tt
+           | @list_rect A P, Compilers.ident.list_rect A' P' => Datatypes.Some tt
+           | @list_case A P, Compilers.ident.list_case A' P' => Datatypes.Some tt
+           | @List_length T, Compilers.ident.List_length T' => Datatypes.Some tt
+           | @List_seq, Compilers.ident.List_seq => Datatypes.Some tt
+           | @List_firstn A, Compilers.ident.List_firstn A' => Datatypes.Some tt
+           | @List_skipn A, Compilers.ident.List_skipn A' => Datatypes.Some tt
+           | @List_repeat A, Compilers.ident.List_repeat A' => Datatypes.Some tt
+           | @List_combine A B, Compilers.ident.List_combine A' B' => Datatypes.Some tt
+           | @List_map A B, Compilers.ident.List_map A' B' => Datatypes.Some tt
+           | @List_app A, Compilers.ident.List_app A' => Datatypes.Some tt
+           | @List_rev A, Compilers.ident.List_rev A' => Datatypes.Some tt
+           | @List_flat_map A B, Compilers.ident.List_flat_map A' B' => Datatypes.Some tt
+           | @List_partition A, Compilers.ident.List_partition A' => Datatypes.Some tt
+           | @List_fold_right A B, Compilers.ident.List_fold_right A' B' => Datatypes.Some tt
+           | @List_update_nth T, Compilers.ident.List_update_nth T' => Datatypes.Some tt
+           | @List_nth_default T, Compilers.ident.List_nth_default T' => Datatypes.Some tt
+           | @Z_add, Compilers.ident.Z_add => Datatypes.Some tt
+           | @Z_mul, Compilers.ident.Z_mul => Datatypes.Some tt
+           | @Z_pow, Compilers.ident.Z_pow => Datatypes.Some tt
+           | @Z_sub, Compilers.ident.Z_sub => Datatypes.Some tt
+           | @Z_opp, Compilers.ident.Z_opp => Datatypes.Some tt
+           | @Z_div, Compilers.ident.Z_div => Datatypes.Some tt
+           | @Z_modulo, Compilers.ident.Z_modulo => Datatypes.Some tt
+           | @Z_log2, Compilers.ident.Z_log2 => Datatypes.Some tt
+           | @Z_log2_up, Compilers.ident.Z_log2_up => Datatypes.Some tt
+           | @Z_eqb, Compilers.ident.Z_eqb => Datatypes.Some tt
+           | @Z_leb, Compilers.ident.Z_leb => Datatypes.Some tt
+           | @Z_ltb, Compilers.ident.Z_ltb => Datatypes.Some tt
+           | @Z_geb, Compilers.ident.Z_geb => Datatypes.Some tt
+           | @Z_gtb, Compilers.ident.Z_gtb => Datatypes.Some tt
+           | @Z_of_nat, Compilers.ident.Z_of_nat => Datatypes.Some tt
+           | @Z_to_nat, Compilers.ident.Z_to_nat => Datatypes.Some tt
+           | @Z_shiftr, Compilers.ident.Z_shiftr => Datatypes.Some tt
+           | @Z_shiftl, Compilers.ident.Z_shiftl => Datatypes.Some tt
+           | @Z_land, Compilers.ident.Z_land => Datatypes.Some tt
+           | @Z_lor, Compilers.ident.Z_lor => Datatypes.Some tt
+           | @Z_min, Compilers.ident.Z_min => Datatypes.Some tt
+           | @Z_max, Compilers.ident.Z_max => Datatypes.Some tt
+           | @Z_bneg, Compilers.ident.Z_bneg => Datatypes.Some tt
+           | @Z_lnot_modulo, Compilers.ident.Z_lnot_modulo => Datatypes.Some tt
+           | @Z_mul_split, Compilers.ident.Z_mul_split => Datatypes.Some tt
+           | @Z_add_get_carry, Compilers.ident.Z_add_get_carry => Datatypes.Some tt
+           | @Z_add_with_carry, Compilers.ident.Z_add_with_carry => Datatypes.Some tt
+           | @Z_add_with_get_carry, Compilers.ident.Z_add_with_get_carry => Datatypes.Some tt
+           | @Z_sub_get_borrow, Compilers.ident.Z_sub_get_borrow => Datatypes.Some tt
+           | @Z_sub_with_get_borrow, Compilers.ident.Z_sub_with_get_borrow => Datatypes.Some tt
+           | @Z_zselect, Compilers.ident.Z_zselect => Datatypes.Some tt
+           | @Z_add_modulo, Compilers.ident.Z_add_modulo => Datatypes.Some tt
+           | @Z_rshi, Compilers.ident.Z_rshi => Datatypes.Some tt
+           | @Z_cc_m, Compilers.ident.Z_cc_m => Datatypes.Some tt
+           | @Z_cast, Compilers.ident.Z_cast range' => Datatypes.Some (range', tt)
+           | @Z_cast2, Compilers.ident.Z_cast2 range' => Datatypes.Some (range', tt)
+           | @option_Some A, Compilers.ident.option_Some A' => Datatypes.Some tt
+           | @option_None A, Compilers.ident.option_None A' => Datatypes.Some tt
+           | @option_rect A P, Compilers.ident.option_rect A' P' => Datatypes.Some tt
+           | @Build_zrange, Compilers.ident.Build_zrange => Datatypes.Some tt
+           | @zrange_rect P, Compilers.ident.zrange_rect P' => Datatypes.Some tt
+           | @fancy_add, Compilers.ident.fancy_add log2wordmax' imm' => Datatypes.Some (log2wordmax', (imm', tt))
+           | @fancy_addc, Compilers.ident.fancy_addc log2wordmax' imm' => Datatypes.Some (log2wordmax', (imm', tt))
+           | @fancy_sub, Compilers.ident.fancy_sub log2wordmax' imm' => Datatypes.Some (log2wordmax', (imm', tt))
+           | @fancy_subb, Compilers.ident.fancy_subb log2wordmax' imm' => Datatypes.Some (log2wordmax', (imm', tt))
+           | @fancy_mulll, Compilers.ident.fancy_mulll log2wordmax' => Datatypes.Some (log2wordmax', tt)
+           | @fancy_mullh, Compilers.ident.fancy_mullh log2wordmax' => Datatypes.Some (log2wordmax', tt)
+           | @fancy_mulhl, Compilers.ident.fancy_mulhl log2wordmax' => Datatypes.Some (log2wordmax', tt)
+           | @fancy_mulhh, Compilers.ident.fancy_mulhh log2wordmax' => Datatypes.Some (log2wordmax', tt)
+           | @fancy_rshi, Compilers.ident.fancy_rshi log2wordmax' x' => Datatypes.Some (log2wordmax', (x', tt))
+           | @fancy_selc, Compilers.ident.fancy_selc => Datatypes.Some tt
+           | @fancy_selm, Compilers.ident.fancy_selm log2wordmax' => Datatypes.Some (log2wordmax', tt)
+           | @fancy_sell, Compilers.ident.fancy_sell => Datatypes.Some tt
+           | @fancy_addm, Compilers.ident.fancy_addm => Datatypes.Some tt
            | @Literal _, _
            | @Nat_succ, _
            | @Nat_pred, _
@@ -2392,13 +2588,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @Z_log2_up, _
            | @Z_eqb, _
            | @Z_leb, _
+           | @Z_ltb, _
            | @Z_geb, _
+           | @Z_gtb, _
            | @Z_of_nat, _
            | @Z_to_nat, _
            | @Z_shiftr, _
            | @Z_shiftl, _
            | @Z_land, _
            | @Z_lor, _
+           | @Z_min, _
+           | @Z_max, _
            | @Z_bneg, _
            | @Z_lnot_modulo, _
            | @Z_mul_split, _
@@ -2413,6 +2613,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @Z_cc_m, _
            | @Z_cast, _
            | @Z_cast2, _
+           | @option_Some _, _
+           | @option_None _, _
+           | @option_rect _ _, _
+           | @Build_zrange, _
+           | @zrange_rect _, _
            | @fancy_add, _
            | @fancy_addc, _
            | @fancy_sub, _
@@ -2426,7 +2631,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @fancy_selm, _
            | @fancy_sell, _
            | @fancy_addm, _
-             => None
+             => Datatypes.None
            end%cps.
 
       Definition of_typed_ident {t} (idc : Compilers.ident.ident t) : ident (type.relax t)
@@ -2475,13 +2680,17 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | Compilers.ident.Z_log2_up => @Z_log2_up
            | Compilers.ident.Z_eqb => @Z_eqb
            | Compilers.ident.Z_leb => @Z_leb
+           | Compilers.ident.Z_ltb => @Z_ltb
            | Compilers.ident.Z_geb => @Z_geb
+           | Compilers.ident.Z_gtb => @Z_gtb
            | 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_min => @Z_min
+           | Compilers.ident.Z_max => @Z_max
            | Compilers.ident.Z_bneg => @Z_bneg
            | Compilers.ident.Z_lnot_modulo => @Z_lnot_modulo
            | Compilers.ident.Z_mul_split => @Z_mul_split
@@ -2496,6 +2705,11 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | Compilers.ident.Z_cc_m => @Z_cc_m
            | Compilers.ident.Z_cast range => @Z_cast
            | Compilers.ident.Z_cast2 range => @Z_cast2
+           | Compilers.ident.option_Some A => @option_Some (base.relax A)
+           | Compilers.ident.option_None A => @option_None (base.relax A)
+           | Compilers.ident.option_rect A P => @option_rect (base.relax A) (base.relax P)
+           | Compilers.ident.Build_zrange => @Build_zrange
+           | Compilers.ident.zrange_rect P => @zrange_rect (base.relax P)
            | Compilers.ident.fancy_add log2wordmax imm => @fancy_add
            | Compilers.ident.fancy_addc log2wordmax imm => @fancy_addc
            | Compilers.ident.fancy_sub log2wordmax imm => @fancy_sub
diff --git a/src/GENERATEDIdentifiersWithoutTypesProofs.v b/src/GENERATEDIdentifiersWithoutTypesProofs.v
index c1b4232d8..9094a8a98 100644
--- a/src/GENERATEDIdentifiersWithoutTypesProofs.v
+++ b/src/GENERATEDIdentifiersWithoutTypesProofs.v
@@ -21,6 +21,7 @@ Module Compilers.
 
   Module pattern.
     Import GENERATEDIdentifiersWithoutTypes.Compilers.pattern.
+    Import Datatypes. (* for Some, None, option *)
 
     Local Lemma quick_invert_eq_option {A} (P : Type) (x y : option A) (H : x = y)
       : match x, y return Type with
@@ -81,6 +82,7 @@ Module Compilers.
     Module Raw.
       Module ident.
         Import GENERATEDIdentifiersWithoutTypes.Compilers.pattern.Raw.ident.
+        Import Datatypes. (* for Some, None, option *)
 
         Global Instance eq_ident_Decidable : DecidableRel (@eq ident) := ident_eq_dec.
 
@@ -144,6 +146,7 @@ Module Compilers.
 
     Module ident.
       Import GENERATEDIdentifiersWithoutTypes.Compilers.pattern.ident.
+      Import Datatypes. (* for Some, None, option *)
 
       Lemma eta_ident_cps_correct T t idc f
         : @eta_ident_cps T t idc f = f t idc.
@@ -201,35 +204,6 @@ Module Compilers.
                             end
                           | progress Compilers.type.inversion_type ].
       Qed.
-
-      (*
-      Local Ltac solve_ex_or_eq :=
-        lazymatch goal with
-        | [ |- ex _ ] => eexists; solve_ex_or_eq
-        | [ |- _ /\ _ ] => split; solve_ex_or_eq
-        | [ |- _ \/ _ ] => (left + right); solve_ex_or_eq
-        | [ |- _ = _ ] => reflexivity || eassumption
-        end.
-      Lemma type_vars_enough
-        : forall t idc k,
-          PositiveSet.mem k (pattern.type.collect_vars t) = true
-          -> exists v, List.In v (@pattern.ident.type_vars t idc) /\ PositiveSet.mem k (pattern.type.collect_vars v) = true.
-      Proof using Type.
-        destruct idc; cbn [type.collect_vars ident.type_vars List.In base.collect_vars PositiveSet.mem PositiveSet.empty PositiveSet.union] in *.
-        all: repeat first [ match goal with
-                            | [ H : true = false |- _ ] => exfalso; apply Bool.diff_true_false, H
-                            | [ H : false = true |- _ ] => exfalso; apply Bool.diff_false_true, H
-                            | [ H : context[PositiveSet.mem _ (PositiveSet.union _ _)] |- _ ]
-                              => rewrite PositiveSetFacts.union_b in H
-                            | [ H : context[orb _ _ = true] |- _ ]
-                              => rewrite Bool.orb_true_iff in H
-                            end
-                          | progress cbn [PositiveSet.mem PositiveSet.empty] in *
-                          | progress intros
-                          | progress destruct_head'_or
-                          | solve_ex_or_eq ].
-      Qed.
-       *)
     End ident.
   End pattern.
 End Compilers.
diff --git a/src/Language.v b/src/Language.v
index efcc16b63..044d19a3e 100644
--- a/src/Language.v
+++ b/src/Language.v
@@ -15,7 +15,7 @@ Require Import Crypto.Util.CPSNotations.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Tactics.RunTacticAsConstr.
 Require Import Crypto.Util.Tactics.DebugPrint.
-Import ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope.
+Import Coq.Lists.List ListNotations. Local Open Scope bool_scope. Local Open Scope Z_scope.
 
 Module Compilers.
   Local Set Boolean Equality Schemes.
@@ -293,8 +293,8 @@ Module Compilers.
   Module base.
     Local Notation einterp := type.interp.
     Module type.
-      Inductive base := unit | Z | bool | nat. (* Not Variant because COQBUG(https://github.com/coq/coq/issues/7738) *)
-      Inductive type := type_base (t : base) | prod (A B : type) | list (A : type).
+      Inductive base := unit | Z | bool | nat | zrange. (* Not Variant because COQBUG(https://github.com/coq/coq/issues/7738) *)
+      Inductive type := type_base (t : base) | prod (A B : type) | list (A : type) | option (A : type).
       Global Coercion type_base : base >-> type.
     End type.
     Global Coercion type.type_base : type.base >-> type.type.
@@ -305,12 +305,14 @@ Module Compilers.
          | type.Z => BinInt.Z
          | type.bool => Datatypes.bool
          | type.nat => Datatypes.nat
+         | type.zrange => zrange
          end.
     Fixpoint interp (ty : type)
       := match ty with
          | type.type_base t => base_interp t
          | type.prod A B => interp A * interp B
          | type.list A => Datatypes.list (interp A)
+         | type.option A => Datatypes.option (interp A)
          end%type.
 
     Definition try_make_base_transport_cps
@@ -321,11 +323,13 @@ Module Compilers.
          | type.Z, type.Z
          | type.bool, type.bool
          | type.nat, type.nat
+         | type.zrange, type.zrange
            => (return (Some id))
          | type.unit, _
          | type.Z, _
          | type.bool, _
          | type.nat, _
+         | type.zrange, _
            => (return None)
          end%cps.
     Fixpoint try_make_transport_cps
@@ -339,9 +343,11 @@ Module Compilers.
                 trB <-- try_make_transport_cps (fun B => P (type.prod _ B)) _ _;
               return (Some (fun v => trB (trA v))))
          | type.list A, type.list A' => try_make_transport_cps (fun A => P (type.list A)) A A'
+         | type.option A, type.option A' => try_make_transport_cps (fun A => P (type.option A)) A A'
          | type.type_base _, _
          | type.prod _ _, _
          | type.list _, _
+         | type.option _, _
            => (return None)
          end%cps.
 
@@ -351,31 +357,6 @@ Module Compilers.
 
     Definition try_transport (P : type -> Type) (t1 t2 : type) (v : P t1) : option (P t2)
       := try_transport_cps P t1 t2 v _ id.
-    (*
-    Fixpoint try_transport
-             (P : type -> Type) (t1 t2 : type) : P t1 -> option (P t2)
-      := match t1, t2 return P t1 -> option (P t2) with
-         | type.unit, type.unit
-         | type.Z, type.Z
-         | type.bool, type.bool
-         | type.nat, type.nat
-           => @Some _
-         | type.list A, type.list A'
-           => @try_transport (fun A => P (type.list A)) A A'
-         | type.prod s d, type.prod s' d'
-           => fun v
-              => (v <- (try_transport (fun s => P (type.prod s d)) s s' v);
-                    (try_transport (fun d => P (type.prod s' d)) d d' v))%option
-
-         | type.unit, _
-         | type.Z, _
-         | type.bool, _
-         | type.nat, _
-         | type.prod _ _, _
-         | type.list _, _
-           => fun _ => None
-         end.
-     *)
 
     Ltac reify_base ty :=
       let __ := Reify.debug_enter_reify_base_type ty in
@@ -384,6 +365,7 @@ Module Compilers.
       | Datatypes.nat => type.nat
       | Datatypes.bool => type.bool
       | BinInt.Z => type.Z
+      | zrange => type.zrange
       | interp (type.type_base ?T) => T
       | @einterp type interp (@Compilers.type.base type (type.type_base ?T)) => T
       | _ => let __ := match goal with
@@ -401,6 +383,9 @@ Module Compilers.
       | Datatypes.list ?T
         => let rT := reify T in
           constr:(type.list rT)
+      | Datatypes.option ?T
+        => let rT := reify T in
+          constr:(type.option rT)
       | interp ?T => T
       | @einterp type interp (@Compilers.type.base type ?T) => T
       | ?ty => let rT := reify_base ty in
@@ -616,6 +601,9 @@ Module Compilers.
         | match ?x with Datatypes.pair a b => @?f a b end
           => let T := type of term in
              reify_rec (@prod_rect _ _ (fun _ => T) f x)
+        | match ?x with ZRange.Build_zrange a b => @?f a b end
+          => let T := type of term in
+             reify_rec (@ZRange.zrange_rect (fun _ => T) f x)
         | match ?x with nil => ?N | cons a b => @?C a b end
           => let T := type of term in
              reify_rec (@list_case _ (fun _ => T) N C x)
@@ -892,13 +880,17 @@ Module Compilers.
         | Z_log2_up : ident (Z -> Z)
         | Z_eqb : ident (Z -> Z -> bool)
         | Z_leb : ident (Z -> Z -> bool)
+        | Z_ltb : ident (Z -> Z -> bool)
         | Z_geb : ident (Z -> Z -> bool)
+        | Z_gtb : ident (Z -> Z -> bool)
         | Z_of_nat : ident (nat -> Z)
         | Z_to_nat : ident (Z -> nat)
         | Z_shiftr : ident (Z -> Z -> Z)
         | Z_shiftl : ident (Z -> Z -> Z)
         | Z_land : ident (Z -> Z -> Z)
         | Z_lor : ident (Z -> Z -> Z)
+        | Z_min : ident (Z -> Z -> Z)
+        | Z_max : ident (Z -> Z -> Z)
         | Z_bneg : ident (Z -> Z)
         | Z_lnot_modulo : ident (Z -> Z -> Z)
         | Z_mul_split : ident (Z -> Z -> Z -> Z * Z)
@@ -911,8 +903,13 @@ Module Compilers.
         | Z_add_modulo : ident (Z -> Z -> Z -> Z)
         | Z_rshi : ident (Z -> Z -> Z -> Z -> Z)
         | Z_cc_m : ident (Z -> Z -> Z)
-        | Z_cast (range : zrange) : ident (Z -> Z)
-        | Z_cast2 (range : zrange * zrange) : ident ((Z * Z) -> (Z * Z))
+        | Z_cast (range : ZRange.zrange) : ident (Z -> Z)
+        | Z_cast2 (range : ZRange.zrange * ZRange.zrange) : ident ((Z * Z) -> (Z * Z))
+        | option_Some {A:base.type} : ident (A -> option A)
+        | option_None {A:base.type} : ident (option A)
+        | option_rect {A P : base.type} : ident ((A -> P) -> (unit -> P) -> option A -> P)
+        | Build_zrange : ident (Z -> Z -> zrange)
+        | zrange_rect {P:base.type} : ident ((Z -> Z -> P) -> zrange -> P)
         | fancy_add (log2wordmax : BinInt.Z) (imm : BinInt.Z) : ident (Z * Z -> Z * Z)
         | fancy_addc (log2wordmax : BinInt.Z) (imm : BinInt.Z) : ident (Z * Z * Z -> Z * Z)
         | fancy_sub (log2wordmax : BinInt.Z) (imm : BinInt.Z) : ident (Z * Z -> Z * Z)
@@ -927,30 +924,34 @@ Module Compilers.
         | fancy_sell : ident (Z * Z * Z -> Z)
         | fancy_addm : ident (Z * Z * Z -> Z)
         .
+        Notation Some := option_Some.
+        Notation None := option_None.
 
         Global Arguments Z_cast2 _%zrange_scope.
 
-        Definition to_fancy {s d : base.type} (idc : ident (s -> d)) : option (fancy.ident s d)
-          := match idc in ident t return option match t with
+        Definition to_fancy {s d : base.type} (idc : ident (s -> d)) : Datatypes.option (fancy.ident s d)
+          := match idc in ident t return Datatypes.option match t with
                                                 | type.base s -> type.base d => fancy.ident s d
                                                 | _ => Datatypes.unit
                                                 end%etype with
-             | fancy_add log2wordmax imm => Some (fancy.with_wordmax log2wordmax (fancy.add imm))
-             | fancy_addc log2wordmax imm => Some (fancy.with_wordmax log2wordmax (fancy.addc imm))
-             | fancy_sub log2wordmax imm => Some (fancy.with_wordmax log2wordmax (fancy.sub imm))
-             | fancy_subb log2wordmax imm => Some (fancy.with_wordmax log2wordmax (fancy.subb imm))
-             | fancy_mulll log2wordmax => Some (fancy.with_wordmax log2wordmax fancy.mulll)
-             | fancy_mullh log2wordmax => Some (fancy.with_wordmax log2wordmax fancy.mullh)
-             | fancy_mulhl log2wordmax => Some (fancy.with_wordmax log2wordmax fancy.mulhl)
-             | fancy_mulhh log2wordmax => Some (fancy.with_wordmax log2wordmax fancy.mulhh)
-             | fancy_rshi log2wordmax x => Some (fancy.with_wordmax log2wordmax (fancy.rshi x))
-             | fancy_selc => Some fancy.selc
-             | fancy_selm log2wordmax => Some (fancy.with_wordmax log2wordmax fancy.selm)
-             | fancy_sell => Some fancy.sell
-             | fancy_addm => Some fancy.addm
-             | _ => None
+             | fancy_add log2wordmax imm => Datatypes.Some (fancy.with_wordmax log2wordmax (fancy.add imm))
+             | fancy_addc log2wordmax imm => Datatypes.Some (fancy.with_wordmax log2wordmax (fancy.addc imm))
+             | fancy_sub log2wordmax imm => Datatypes.Some (fancy.with_wordmax log2wordmax (fancy.sub imm))
+             | fancy_subb log2wordmax imm => Datatypes.Some (fancy.with_wordmax log2wordmax (fancy.subb imm))
+             | fancy_mulll log2wordmax => Datatypes.Some (fancy.with_wordmax log2wordmax fancy.mulll)
+             | fancy_mullh log2wordmax => Datatypes.Some (fancy.with_wordmax log2wordmax fancy.mullh)
+             | fancy_mulhl log2wordmax => Datatypes.Some (fancy.with_wordmax log2wordmax fancy.mulhl)
+             | fancy_mulhh log2wordmax => Datatypes.Some (fancy.with_wordmax log2wordmax fancy.mulhh)
+             | fancy_rshi log2wordmax x => Datatypes.Some (fancy.with_wordmax log2wordmax (fancy.rshi x))
+             | fancy_selc => Datatypes.Some fancy.selc
+             | fancy_selm log2wordmax => Datatypes.Some (fancy.with_wordmax log2wordmax fancy.selm)
+             | fancy_sell => Datatypes.Some fancy.sell
+             | fancy_addm => Datatypes.Some fancy.addm
+             | _ => Datatypes.None
              end.
       End with_scope.
+      Notation Some := option_Some.
+      Notation None := option_None.
 
       Section gen.
         Context (cast_outside_of_range : zrange -> BinInt.Z -> BinInt.Z).
@@ -1036,7 +1037,9 @@ Module Compilers.
              | Z_modulo => Z.modulo
              | Z_eqb => Z.eqb
              | Z_leb => Z.leb
+             | Z_ltb => Z.ltb
              | Z_geb => Z.geb
+             | Z_gtb => Z.gtb
              | Z_log2 => Z.log2
              | Z_log2_up => Z.log2_up
              | Z_of_nat => Z.of_nat
@@ -1045,6 +1048,8 @@ Module Compilers.
              | Z_shiftl => Z.shiftl
              | Z_land => Z.land
              | Z_lor => Z.lor
+             | Z_min => Z.min
+             | Z_max => Z.max
              | Z_mul_split => Z.mul_split
              | Z_add_get_carry => Z.add_get_carry_full
              | Z_add_with_carry => Z.add_with_carry
@@ -1059,6 +1064,12 @@ Module Compilers.
              | Z_cc_m => Z.cc_m
              | Z_cast r => cast r
              | Z_cast2 (r1, r2) => fun '(x1, x2) => (cast r1 x1, cast r2 x2)
+             | Some A => @Datatypes.Some _
+             | None A => @Datatypes.None _
+             | option_rect A P
+               => fun S_case N_case o => @Datatypes.option_rect _ _ S_case (N_case tt) o
+             | Build_zrange => ZRange.Build_zrange
+             | zrange_rect A => @ZRange.zrange_rect _
              | fancy_add _ _ as idc
              | fancy_addc _ _ as idc
              | fancy_sub _ _ as idc
@@ -1079,6 +1090,8 @@ Module Compilers.
       Definition cast_outside_of_range (r : zrange) (v : BinInt.Z) : BinInt.Z.
       Proof. exact v. Qed.
     End with_base.
+    Notation Some := option_Some.
+    Notation None := option_None.
 
     (** Interpret identifiers where [Z_cast] is an opaque identity
         function when the value is not inside the range *)
@@ -1087,6 +1100,7 @@ Module Compilers.
     Notation LiteralZ := (@Literal base.type.Z).
     Notation LiteralBool := (@Literal base.type.bool).
     Notation LiteralNat := (@Literal base.type.nat).
+    Notation LiteralZRange := (@Literal base.type.zrange).
 
     (** TODO: MOVE ME? *)
     Module Thunked.
@@ -1098,6 +1112,8 @@ Module Compilers.
         := ListUtil.list_case (fun _ => P) (N tt) C ls.
       Definition nat_rect P (O_case : unit -> P) (S_case : nat -> P -> P) (n : nat) : P
         := Datatypes.nat_rect (fun _ => P) (O_case tt) S_case n.
+      Definition option_rect {A} P (S_case : A -> P) (N_case : unit -> P) (o : option A) : P
+        := Datatypes.option_rect (fun _ => P) S_case (N_case tt) o.
     End Thunked.
 
     Ltac require_primitive_const term :=
@@ -1113,6 +1129,10 @@ Module Compilers.
       | xI ?p => require_primitive_const p
       | xO ?p => require_primitive_const p
       | xH => idtac
+      | Datatypes.Some ?x => require_primitive_const x
+      | Datatypes.None => idtac
+      | ZRange.Build_zrange ?x ?y
+        => require_primitive_const x; require_primitive_const y
       | ?term => fail 0 "Not a known const:" term
       end.
     Ltac is_primitive_const term :=
@@ -1175,6 +1195,16 @@ Module Compilers.
         | @Thunked.bool_rect ?T
           => let rT := base.reify T in
              then_tac (@ident.bool_rect rT)
+        | @Datatypes.option_rect ?A ?T0 ?PSome ?PNone
+          => lazymatch (eval cbv beta in T0) with
+             | fun _ => ?T => reify_rec (@Thunked.option_rect A T PSome (fun _ : Datatypes.unit => PNone))
+             | T0 => else_tac ()
+             | ?T' => reify_rec (@Datatypes.option_rect A T' PSome PNone)
+             end
+        | @Thunked.option_rect ?A ?T
+          => let rA := base.reify A in
+             let rT := base.reify T in
+             then_tac (@ident.option_rect rA rT)
         | @Datatypes.prod_rect ?A ?B ?T0
           => lazymatch (eval cbv beta in T0) with
             | fun _ => ?T
@@ -1185,6 +1215,14 @@ Module Compilers.
             | T0 => else_tac ()
             | ?T' => reify_rec (@Datatypes.prod_rect A B T')
             end
+        | @ZRange.zrange_rect ?T0
+          => lazymatch (eval cbv beta in T0) with
+             | fun _ => ?T
+               => let rT := base.reify T in
+                  then_tac (@ident.zrange_rect rT)
+             | T0 => else_tac ()
+             | ?T' => reify_rec (@ZRange.zrange_rect T')
+             end
         | @Datatypes.nat_rect ?T0 ?P0
           => lazymatch (eval cbv beta in T0) with
              | fun _ => _ -> _ => else_tac ()
@@ -1277,13 +1315,17 @@ Module Compilers.
         | Z.modulo => then_tac ident.Z_modulo
         | Z.eqb => then_tac ident.Z_eqb
         | Z.leb => then_tac ident.Z_leb
+        | Z.ltb => then_tac ident.Z_ltb
         | Z.geb => then_tac ident.Z_geb
+        | Z.gtb => then_tac ident.Z_gtb
         | Z.log2 => then_tac ident.Z_log2
         | Z.log2_up => then_tac ident.Z_log2_up
         | Z.shiftl => then_tac ident.Z_shiftl
         | Z.shiftr => then_tac ident.Z_shiftr
         | Z.land => then_tac ident.Z_land
         | Z.lor => then_tac ident.Z_lor
+        | Z.min => then_tac ident.Z_min
+        | Z.max => then_tac ident.Z_max
         | Z.bneg => then_tac ident.Z_bneg
         | Z.lnot_modulo => then_tac ident.Z_lnot_modulo
         | Z.of_nat => then_tac ident.Z_of_nat
@@ -1298,6 +1340,14 @@ Module Compilers.
         | Z.add_modulo => then_tac ident.Z_add_modulo
         | Z.rshi => then_tac ident.Z_rshi
         | Z.cc_m => then_tac ident.Z_cc_m
+        | ident.cast _ => then_tac ident.Z_cast
+        | @Some ?A
+          => let rA := base.reify A in
+             then_tac (@ident.Some rA)
+        | @None ?A
+          => let rA := base.reify A in
+             then_tac (@ident.None rA)
+        | ZRange.Build_zrange => then_tac ident.Build_zrange
         | _ => else_tac ()
         end
       end.
@@ -1309,6 +1359,13 @@ Module Compilers.
            (fun x _ xs => expr.Ident ident.cons @ x @ xs)%expr
            ls.
 
+    Definition reify_option {var} {t} (v : option (@expr.expr base.type ident var (type.base t))) : @expr.expr base.type ident var (type.base (base.type.option t))
+      := Datatypes.option_rect
+           (fun _ => _)
+           (fun x => expr.Ident ident.Some @ x)%expr
+           (expr.Ident ident.None)
+           v.
+
     Fixpoint smart_Literal {var} {t:base.type} : base.interp t -> @expr.expr base.type ident var (type.base t)
       := match t with
          | base.type.type_base t => fun v => expr.Ident (ident.Literal v)
@@ -1318,6 +1375,9 @@ Module Compilers.
          | base.type.list A
            => fun v : list (base.interp A)
               => reify_list (List.map (@smart_Literal var A) v)
+         | base.type.option A
+           => fun v : option (base.interp A)
+              => reify_option (option_map (@smart_Literal var A) v)
          end%expr.
 
     Module Export Notations.
@@ -1354,7 +1414,7 @@ Module Compilers.
       Notation "x 'mod' y" := (#Z_modulo @ x @ y)%expr : expr_scope.
       Notation "- x" := (#Z_opp @ x)%expr : expr_scope.
       Global Arguments gen_interp _ _ !_.
-
+      Global Arguments ident.Z_cast _%zrange_scope.
       Global Arguments ident.Z_cast2 _%zrange_scope.
     End Notations.
   End ident.
@@ -1519,6 +1579,42 @@ Module Compilers.
            | Some (ident.nil _) => true
            | _ => false
            end.
+      Definition invert_None {t} (e : expr (base.type.option t)) : bool
+        := match invert_Ident e with
+           | Some (ident.None _) => true
+           | _ => false
+           end.
+      Local Notation if_arrow f t
+        := (match t return Type with
+            | (a -> b)%etype => f a b
+            | _ => unit
+            end) (only parsing).
+      Definition invert_Some {t} (e : expr (base.type.option t))
+        : option (expr t)
+        := match invert_AppIdent e with
+           | Some (existT s (idc, e))
+             => match idc in ident.ident t
+                      return if_arrow (fun a b => expr a) t
+                             -> option match t return Type with
+                                       | (a -> type.base (base.type.option t))
+                                         => expr t
+                                       | _ => unit
+                                       end%etype
+                with
+                | ident.Some _ => fun x => Some x
+                | _ => fun _ => None
+                end e
+           | None => None
+           end.
+
+      Definition reflect_option {t} (e : expr (base.type.option t))
+        : option (option (expr t))
+        := match invert_None e, invert_Some e with
+           | true, _ => Some None
+           | _, Some x => Some (Some x)
+           | false, None => None
+           end.
+
       Local Notation if_arrow2 f t
         := (match t return Type with
             | (a -> b -> c)%etype => f a b c
@@ -1590,9 +1686,11 @@ Module Compilers.
              | base.type.Z => (-1)%Z
              | base.type.nat => 0%nat
              | base.type.bool => true
+             | base.type.zrange => r[0~>0]%zrange
              | base.type.list _ => nil
              | base.type.prod A B
                => (@default A, @default B)
+             | base.type.option A => None
              end.
       End base.
       Fixpoint default {t} : type.interp base.interp t
@@ -1611,10 +1709,12 @@ Module Compilers.
                | base.type.prod A B
                  => (@default A, @default B)
                | base.type.list A => #ident.nil
+               | base.type.option A => #ident.None
                | base.type.unit as t
                | base.type.Z as t
                | base.type.nat as t
                | base.type.bool as t
+               | base.type.zrange as t
                  => ##(@type.base.default t)
                end%expr.
         End with_var.
@@ -1649,6 +1749,7 @@ Module Compilers.
   End defaults.
 
   Notation reify_list := ident.reify_list.
+  Notation reify_option := ident.reify_option.
 
   Module GallinaReify.
     Module base.
@@ -1663,10 +1764,14 @@ Module Compilers.
              | base.type.list A as t
                => fun x : list (base.interp A)
                   => reify_list (List.map (@reify A) x)
+             | base.type.option A as t
+               => fun x : option (base.interp A)
+                  => reify_option (option_map (@reify A) x)
              | base.type.unit as t
              | base.type.Z as t
              | base.type.bool as t
              | base.type.nat as t
+             | base.type.zrange as t
                => fun x : base.interp t
                   => (##x)%expr
              end.
diff --git a/src/LanguageInversion.v b/src/LanguageInversion.v
index 7bc86d396..30d7fb3b4 100644
--- a/src/LanguageInversion.v
+++ b/src/LanguageInversion.v
@@ -25,9 +25,11 @@ Module Compilers.
                | base.type.type_base t1, base.type.type_base t2 => t1 = t2
                | base.type.prod A1 B1, base.type.prod A2 B2 => A1 = A2 /\ B1 = B2
                | base.type.list A1, base.type.list A2 => A1 = A2
+               | base.type.option A1, base.type.option A2 => A1 = A2
                | base.type.type_base _, _
                | base.type.prod _ _, _
                | base.type.list _, _
+               | base.type.option _, _
                  => False
                end.
 
@@ -81,6 +83,10 @@ Module Compilers.
                   => induction_type_in_using H @path_rect
                 | [ H : base.type.list _ = _ |- _ ]
                   => induction_type_in_using H @path_rect
+                | [ H : _ = base.type.option _ |- _ ]
+                  => induction_type_in_using H @path_rect
+                | [ H : base.type.option _ = _ |- _ ]
+                  => induction_type_in_using H @path_rect
                 end ];
         cbn [f_equal f_equal2 eq_rect decode] in *.
       Ltac inversion_type := repeat inversion_type_step.
@@ -518,6 +524,39 @@ Module Compilers.
         apply invert_AppIdent2_Some in H; subst; break_innermost_match.
         t.
       Qed.
+      Lemma invert_None_Some {t} {e : expr (base.type.option t)}
+        : invert_expr.invert_None e = true -> e = (#ident.None)%expr.
+      Proof. cbv [invert_expr.invert_None invert_expr.invert_Ident]; t. Qed.
+      Lemma invert_Some_Some {t} {e : expr (base.type.option t)} {v}
+        : invert_expr.invert_Some e = Some v -> e = (#ident.Some @ v)%expr.
+      Proof.
+        cbv [invert_expr.invert_Some].
+        destruct (invert_expr.invert_AppIdent _) eqn:H; [ | congruence ].
+        apply invert_AppIdent_Some in H; subst; break_innermost_match.
+        t.
+      Qed.
+
+      Lemma reify_option_None {t} : reify_option None = (#ident.None)%expr :> expr (base.type.option t).
+      Proof. reflexivity. Qed.
+      Lemma reify_option_Some {t} (x : expr (type.base t)) : reify_option (Some x) = (#ident.Some @ x)%expr.
+      Proof. reflexivity. Qed.
+      Lemma reflect_option_Some {t} {e : expr (base.type.option t)} {v} : invert_expr.reflect_option e = Some v -> e = reify_option v.
+      Proof.
+        cbv [invert_expr.reflect_option].
+        destruct (invert_expr.invert_None _) eqn:H;
+          [ | destruct (invert_expr.invert_Some _) eqn:H' ];
+          try apply invert_None_Some in H;
+          try apply invert_Some_Some in H';
+          intros; inversion_option; subst; reflexivity.
+      Qed.
+      Lemma reflect_option_Some_None {t} {e : expr (base.type.option t)} : invert_expr.reflect_option e = Some None -> e = (#ident.None)%expr.
+      Proof. exact (@reflect_option_Some _ e None). Qed.
+      Lemma reflect_reify_option {t} {v} : invert_expr.reflect_option (var:=var) (reify_option (t:=t) v) = Some v.
+      Proof.
+        destruct v; rewrite ?reify_option_Some, ?reify_option_None; reflexivity.
+      Qed.
+      Lemma reflect_option_Some_iff  {t} {e : expr (base.type.option t)} {v} : invert_expr.reflect_option e = Some v <-> e = reify_option v.
+      Proof. split; intro; subst; apply reflect_reify_option || apply reflect_option_Some; assumption. Qed.
 
       Lemma reflect_list_cps'_id_nil {t} (e : expr _ := (#(@ident.nil t))%expr)
         : forall T k, invert_expr.reflect_list_cps' e T k = k (invert_expr.reflect_list_cps' e _ id).
@@ -676,6 +715,11 @@ Module Compilers.
       | [ H : invert_expr.reflect_list ?e = Some _ |- _ ]
         => guard_tac H; first [ apply reflect_list_Some_nil in H | apply reflect_list_Some in H ];
           rewrite ?reify_list_cons, ?reify_list_nil in H
+      | [ H : invert_expr.invert_None ?e = Some _ |- _ ] => guard_tac H; apply invert_None_Some in H
+      | [ H : invert_expr.invert_Some ?e = Some _ |- _ ] => guard_tac H; apply invert_Some_Some in H
+      | [ H : invert_expr.reflect_option ?e = Some _ |- _ ]
+        => guard_tac H; first [ apply reflect_option_Some_None in H | apply reflect_option_Some in H ];
+          rewrite ?reify_option_Some, ?reify_option_None in H
       end.
     Ltac invert_subst_step :=
       first [ invert_subst_step_helper ltac:(fun _ => idtac)
diff --git a/src/LanguageWf.v b/src/LanguageWf.v
index 7f6bd5e18..1119e1977 100644
--- a/src/LanguageWf.v
+++ b/src/LanguageWf.v
@@ -220,7 +220,7 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
     Proof.
       destruct idc; cbn [type.eqv ident.gen_interp type.interp base.interp base.base_interp];
         try solve [ typeclasses eauto
-                  | cbv [respectful]; repeat intro; subst; destruct_head_hnf bool; destruct_head_hnf prod; eauto
+                  | cbv [respectful]; repeat intro; subst; destruct_head_hnf bool; destruct_head_hnf prod; destruct_head_hnf option; destruct_head_hnf zrange; eauto
                   | cbv [respectful]; repeat intro; (apply nat_rect_Proper_nondep || apply list_rect_Proper || apply list_case_Proper); repeat intro; eauto ].
     Qed.
 
@@ -996,9 +996,58 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
                             | progress expr.invert_match ].
         Qed.
 
+        Lemma wf_reify_option G {t} e1 e2
+          : @wf _ _ var1 var2 G _ (reify_option (t:=t) e1) (reify_option (t:=t) e2)
+            <-> option_eq (wf G) e1 e2.
+        Proof.
+          destruct_head' option; cbn in *; split; intros.
+          all: repeat first [ assumption
+                            | progress inversion_option
+                            | exfalso; assumption
+                            | progress inversion_wf_constr
+                            | progress destruct_head'_sig
+                            | progress destruct_head'_and
+                            | progress type.inversion_type
+                            | constructor ].
+        Qed.
+
+        Lemma wf_reflect_option G {t} e1 e2
+           : @wf _ _ var1 var2 G (type.base (base.type.option t)) e1 e2
+            -> (invert_expr.reflect_option e1 = None <-> invert_expr.reflect_option e2 = None).
+        Proof.
+          destruct (invert_expr.reflect_option e1) eqn:H1, (invert_expr.reflect_option e2) eqn:H2;
+            try (split; congruence); expr.invert_subst;
+              try (revert dependent e2; intro); try (revert dependent e1; intro);
+                match goal with
+                | [ |- context[Some ?l = None] ]
+                  => destruct l
+                end;
+                rewrite ?expr.reify_option_Some, ?expr.reify_option_None;
+                cbv [invert_expr.reflect_option];
+                break_innermost_match; try congruence; intros.
+          all: repeat first [ congruence
+                            | progress inversion_wf_constr
+                            | progress subst
+                            | progress cbv [option_map] in *
+                            | progress destruct_head' False
+                            | progress destruct_head'_sig
+                            | progress destruct_head'_and
+                            | progress inversion_option
+                            | progress inversion_sigma
+                            | progress inversion_prod
+                            | progress type.inversion_type
+                            | progress base.type.inversion_type
+                            | progress break_match_hyps
+                            | progress cbn [fst snd invert_expr.invert_Ident invert_expr.invert_None invert_expr.invert_Some invert_expr.invert_AppIdent invert_expr.invert_Ident invert_expr.invert_App2 invert_expr.invert_App Option.bind fst snd projT1 projT2 eq_rect] in *
+                            | progress expr.invert_subst
+                            | solve [ eauto ]
+                            | progress inversion_wf_one_constr
+                            | progress expr.invert_match ].
+        Qed.
+
         Lemma wf_reify {t} v G : expr.wf G (@GallinaReify.base.reify var1 t v) (@GallinaReify.base.reify var2 t v).
         Proof.
-          induction t; cbn; break_innermost_match; repeat constructor; auto; [].
+          induction t; cbn; cbv [option_map]; break_innermost_match; repeat constructor; auto; [].
           rewrite wf_reify_list, !map_length, combine_map_map, combine_same, map_map; split; auto; intros *; [].
           cbn [fst snd]; rewrite in_map_iff; intros.
           repeat first [ progress destruct_head'_and
@@ -1026,11 +1075,13 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
               reflexivity.
         Qed.
 
+        Lemma interp_reify_option {t} v : interp (reify_option (t:=t) v) = Option.map interp v.
+        Proof. destruct v; reflexivity. Qed.
+
         Lemma interp_smart_Literal {t} v : interp (@ident.smart_Literal _ t v) = v.
         Proof.
           cbv [ident.interp]; induction t; cbn [ident.smart_Literal expr.interp ident.gen_interp];
-            break_innermost_match; cbn [expr.interp ident.gen_interp].
-          { reflexivity. }
+            break_innermost_match; cbn [expr.interp ident.gen_interp]; cbv [option_map]; break_innermost_match; cbn; rewrite ?IHt; try reflexivity.
           { apply f_equal2; auto. }
           { etransitivity; [ rewrite interp_reify_list, map_map | apply map_id ].
             apply map_ext; auto. }
@@ -1038,7 +1089,7 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
 
         Lemma interp_reify {t} v : interp (GallinaReify.base.reify (t:=t) v) = v.
         Proof.
-          induction t; cbn [GallinaReify.base.reify]; break_innermost_match; cbn; f_equal;
+          induction t; cbn [GallinaReify.base.reify]; cbv [option_map]; break_innermost_match; cbn; f_equal;
             rewrite ?interp_reify_list, ?map_map; auto.
           { etransitivity; [ | apply map_id ]; apply map_ext; auto. }
         Qed.
@@ -1065,7 +1116,7 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
 
   Hint Constructors expr.wf : wf.
   Hint Resolve @expr.Wf_APP expr.Wf_Reify expr.Wf_reify : wf.
-  Hint Rewrite @expr.Interp_Reify @expr.interp_reify @expr.interp_reify_list @expr.Interp_reify @expr.Interp_APP : interp.
+  Hint Rewrite @expr.Interp_Reify @expr.interp_reify @expr.interp_reify_list @expr.interp_reify_option @expr.Interp_reify @expr.Interp_APP : interp.
 
   Notation Wf := expr.Wf.
 
diff --git a/src/Rewriter.v b/src/Rewriter.v
index a79bcb18f..e23b65ae7 100644
--- a/src/Rewriter.v
+++ b/src/Rewriter.v
@@ -41,6 +41,7 @@ Module Compilers.
            | type.type_base t => type.type_base t
            | type.prod A B => type.prod (partial_subst A evar_map) (partial_subst B evar_map)
            | type.list A => type.list (partial_subst A evar_map)
+           | type.option A => type.option (partial_subst A evar_map)
            end.
 
       Fixpoint subst (ptype : type) (evar_map : EvarMap) : option Compilers.base.type
@@ -52,6 +53,7 @@ Module Compilers.
                    B' <- subst B evar_map;
                    Some (Compilers.base.type.prod A' B'))
            | type.list A => option_map Compilers.base.type.list (subst A evar_map)
+           | type.option A => option_map Compilers.base.type.option (subst A evar_map)
            end%option.
 
       Fixpoint subst_default_relax P {t evm} : P t -> P (subst_default (relax t) evm)
@@ -66,6 +68,8 @@ Module Compilers.
                         v)
            | Compilers.base.type.list A
              => @subst_default_relax (fun t => P (Compilers.base.type.list t)) A evm
+           | Compilers.base.type.option A
+             => @subst_default_relax (fun t => P (Compilers.base.type.option t)) A evm
            end.
 
       Fixpoint var_types_of (t : type) : Set
@@ -74,6 +78,7 @@ Module Compilers.
            | type.type_base _ => unit
            | type.prod A B => var_types_of A * var_types_of B
            | type.list A => var_types_of A
+           | type.option A => var_types_of A
            end%type.
 
       Fixpoint add_var_types_cps {t : type} (v : var_types_of t) (evm : EvarMap) : ~> EvarMap
@@ -84,6 +89,7 @@ Module Compilers.
               | type.prod A B
                 => fun '(a, b) => @add_var_types_cps A a evm _ (fun evm => @add_var_types_cps B b evm _ k)
               | type.list A => fun t => @add_var_types_cps A t evm _ k
+              | type.option A => fun t => @add_var_types_cps A t evm _ k
               | type.type_base _ => fun _ => k evm
               end v.
 
@@ -102,9 +108,12 @@ Module Compilers.
                   Some (a, b)
            | type.list A, Compilers.base.type.list A'
              => unify_extracted A A'
+           | type.option A, Compilers.base.type.option A'
+             => unify_extracted A A'
            | type.type_base _, _
            | type.prod _ _, _
            | type.list _, _
+           | type.option _, _
              => None
            end%option.
     End base.
@@ -1231,6 +1240,7 @@ Module Compilers.
                     b <- make_Literal_pattern B;
                     Some ((#pattern.ident.pair @ a @ b)%pattern))
              | pattern.base.type.list A => None
+             | pattern.base.type.option A => None
              end%option%cps.
 
         Fixpoint make_interp_rewrite_pattern {t}
@@ -1272,6 +1282,7 @@ Module Compilers.
                  with
                  | pattern.base.type.var _
                  | pattern.base.type.list _
+                 | pattern.base.type.option _
                    => I
                  | pattern.base.type.type_base t
                    => fun f x => f x
@@ -1937,13 +1948,13 @@ Module Compilers.
       Definition strip_literal_casts_dtree'
         := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 strip_literal_casts_rewrite_rules.
       Definition nbe_dtree : decision_tree
-        := Eval compute in invert_Some nbe_dtree'.
+        := Eval compute in Option.invert_Some nbe_dtree'.
       Definition arith_dtree : decision_tree
-        := Eval compute in invert_Some arith_dtree'.
+        := Eval compute in Option.invert_Some arith_dtree'.
       Definition arith_with_casts_dtree : decision_tree
-        := Eval compute in invert_Some arith_with_casts_dtree'.
+        := Eval compute in Option.invert_Some arith_with_casts_dtree'.
       Definition strip_literal_casts_dtree : decision_tree
-        := Eval compute in invert_Some strip_literal_casts_dtree'.
+        := Eval compute in Option.invert_Some strip_literal_casts_dtree'.
 
       Definition nbe_default_fuel := Eval compute in List.length nbe_rewrite_rules.
       Definition arith_default_fuel := Eval compute in List.length (arith_rewrite_rules 0%Z (* dummy val *)).
@@ -2214,11 +2225,11 @@ Z.mul @@ (?x >> 128, ?y >> 128)             --> mulhh @@ (x, y)
         Definition fancy_dtree'
           := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 fancy_rewrite_rules.
         Definition fancy_dtree : decision_tree
-          := Eval compute in invert_Some fancy_dtree'.
+          := Eval compute in Option.invert_Some fancy_dtree'.
         Definition fancy_with_casts_dtree'
           := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 fancy_with_casts_rewrite_rules.
         Definition fancy_with_casts_dtree : decision_tree
-          := Eval compute in invert_Some fancy_with_casts_dtree'.
+          := Eval compute in Option.invert_Some fancy_with_casts_dtree'.
         Definition fancy_default_fuel := Eval compute in List.length fancy_rewrite_rules.
         Definition fancy_with_casts_default_fuel := Eval compute in List.length fancy_with_casts_rewrite_rules.
         Import PrimitiveHList.
@@ -2255,8 +2266,8 @@ Z.mul @@ (?x >> 128, ?y >> 128)             --> mulhh @@ (x, y)
       Export Language.Compilers.defaults.
       Export PrimitiveSigma.Primitive.
       Notation "'llet' x := v 'in' f" := (Let_In v (fun x => f)).
-      Notation "x <- 'type.try_make_transport_cps' t1 t2 ; f" := (type.try_make_transport_cps t1 t2 (fun y => match y with Some x => f | None => None end)) (at level 70, t1 at next level, t2 at next level, right associativity, format "'[v' x  <-  'type.try_make_transport_cps'  t1  t2 ; '/' f ']'").
-      Notation "x <- 'base.try_make_transport_cps' t1 t2 ; f" := (base.try_make_transport_cps t1 t2 (fun y => match y with Some x => f | None => None end)) (at level 70, t1 at next level, t2 at next level, right associativity, format "'[v' x  <-  'base.try_make_transport_cps'  t1  t2 ; '/' f ']'").
+      Notation "x <- 'type.try_make_transport_cps' t1 t2 ; f" := (type.try_make_transport_cps t1 t2 (fun y => match y with Datatypes.Some x => f | Datatypes.None => Datatypes.None end)) (at level 70, t1 at next level, t2 at next level, right associativity, format "'[v' x  <-  'type.try_make_transport_cps'  t1  t2 ; '/' f ']'").
+      Notation "x <- 'base.try_make_transport_cps' t1 t2 ; f" := (base.try_make_transport_cps t1 t2 (fun y => match y with Datatypes.Some x => f | Datatypes.None => Datatypes.None end)) (at level 70, t1 at next level, t2 at next level, right associativity, format "'[v' x  <-  'base.try_make_transport_cps'  t1  t2 ; '/' f ']'").
     End RewriterPrintingNotations.
 
     Ltac make_rewrite_head1 rewrite_head0 pr2_rewrite_rules :=
diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v
index f425a769b..0ec6396f2 100644
--- a/src/RewriterWf1.v
+++ b/src/RewriterWf1.v
@@ -71,6 +71,7 @@ Module Compilers.
                          | progress intros
                          | reflexivity
                          | apply (f_equal base.type.list)
+                         | apply (f_equal base.type.option)
                          | apply (f_equal2 base.type.prod)
                          | break_innermost_match_step
                          | break_innermost_match_hyps_step
@@ -126,6 +127,7 @@ Module Compilers.
                          | [ |- iff _ _ ] => split
                          | [ H : base.type.prod _ _ = base.type.prod _ _ |- _ ] => inversion H; clear H
                          | [ H : base.type.list _ = base.type.list _ |- _ ] => inversion H; clear H
+                         | [ H : base.type.option _ = base.type.option _ |- _ ] => inversion H; clear H
                          | [ H : Some _ = _ |- _ ] => symmetry in H
                          | [ H : None = _ |- _ ] => symmetry in H
                          | [ H : ?x = Some _ |- context[?x] ] => rewrite H
diff --git a/src/UnderLets.v b/src/UnderLets.v
index 522a8c4c7..34cecf322 100644
--- a/src/UnderLets.v
+++ b/src/UnderLets.v
@@ -108,6 +108,13 @@ Module Compilers.
              => splice x (fun x => @splice_list A B xs (fun xs => e (cons x xs)))
            end.
 
+      Definition splice_option {A B} (v : option (@UnderLets A)) (e : option A -> @UnderLets B) : @UnderLets B
+        := match v with
+           | None => e None
+           | Some x
+             => splice x (fun x => e (Some x))
+           end.
+
       Fixpoint to_expr {t} (x : @UnderLets (expr t)) : expr t
         := match x with
            | Base v => v
@@ -127,6 +134,7 @@ Module Compilers.
       Bind Scope under_lets_scope with UnderLets.UnderLets.
       Notation "x <-- y ; f" := (UnderLets.splice y (fun x => f%under_lets)) : under_lets_scope.
       Notation "x <---- y ; f" := (UnderLets.splice_list y (fun x => f%under_lets)) : under_lets_scope.
+      Notation "x <----- y ; f" := (UnderLets.splice_option y (fun x => f%under_lets)) : under_lets_scope.
     End Notations.
 
     Section reify.
@@ -183,6 +191,22 @@ Module Compilers.
                           k
                    | None => @default_reify_and_let_binds_base_cps _ e T k
                    end
+           | base.type.option A
+             => fun e T k
+                => match reflect_option e with
+                   | Some ls
+                     => option_rect
+                          _
+                          (fun x k
+                           => @reify_and_let_binds_base_cps
+                                A x _
+                                (fun xe
+                                 => k (#ident.Some @ xe)%expr))
+                          (fun k => k (#ident.None)%expr)
+                          ls
+                          k
+                   | None => @default_reify_and_let_binds_base_cps _ e T k
+                   end
            end%under_lets.
 
       Fixpoint let_bind_return {t} : expr t -> expr t
diff --git a/src/UnderLetsProofs.v b/src/UnderLetsProofs.v
index 884b6687a..72c3ff53d 100644
--- a/src/UnderLetsProofs.v
+++ b/src/UnderLetsProofs.v
@@ -652,8 +652,9 @@ Module Compilers.
           : wf P G (reify_and_let_binds_base_cps e1 T1 k1) (reify_and_let_binds_base_cps e2 T2 k2).
         Proof.
           revert dependent G; induction t; cbn [reify_and_let_binds_base_cps]; intros;
+            cbv [option_rect];
             try (cbv [SubstVarLike.is_var_fst_snd_pair_opp_cast] in *; erewrite !SubstVarLike.wfT_is_recursively_var_or_ident by eassumption);
-            break_innermost_match; wf_reify_and_let_binds_base_cps_t Hk.
+            break_innermost_match; wf_reify_and_let_binds_base_cps_t Hk; eauto.
           all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end.
           all: revert dependent k1; revert dependent k2.
           all: lazymatch goal with
@@ -719,13 +720,14 @@ Module Compilers.
           : P (UnderLets.interp (@ident_interp) (@reify_and_let_binds_base_cps _ t e T k)).
         Proof.
           revert T k P Hk; induction t; cbn [reify_and_let_binds_base_cps]; intros;
-            break_innermost_match;
+            cbv [option_rect]; break_innermost_match;
             expr.invert_subst; cbn [type.related UnderLets.interp fst snd expr.interp ident_interp] in *; subst; eauto;
               repeat first [ progress intros
                            | reflexivity
                            | progress cbn [expr.interp ident_interp List.map]
                            | apply (f_equal2 (@pair _ _))
                            | apply (f_equal2 (@cons _))
+                           | apply (f_equal (@Some _))
                            | match goal with
                              | [ H : _ |- _ ] => apply H; clear H
                              | [ H : SubstVarLike.is_var_fst_snd_pair_opp_cast (reify_list _) = _ |- _ ] => clear H
@@ -823,6 +825,7 @@ Module Compilers.
           : interp (to_expr (reify_and_let_binds_base_cps e1 _ k1)) == k2 (interp e2).
         Proof.
           revert dependent G; revert dependent t'; induction t; cbn [reify_and_let_binds_base_cps]; intros;
+            cbv [option_rect];
             try (cbv [SubstVarLike.is_var_fst_snd_pair_opp_cast] in *; erewrite !SubstVarLike.wfT_is_recursively_var_or_ident by eassumption);
             break_innermost_match; interp_to_expr_reify_and_let_binds_base_cps_t Hk.
           all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end.
@@ -950,7 +953,7 @@ Module Compilers.
         Proof using Type.
           cbv [expr.interp_related]; revert T T' k R v; induction t.
           all: repeat first [ progress cbn [expr.interp_related_gen interp_related reify_and_let_binds_base_cps fst snd] in *
-                            | progress cbv [expr.interp_related] in *
+                            | progress cbv [expr.interp_related option_rect] in *
                             | progress intros
                             | assumption
                             | progress destruct_head'_ex
-- 
cgit v1.2.3