diff options
Diffstat (limited to 'src/nbe_rewrite_head.out')
| -rw-r--r-- | src/nbe_rewrite_head.out | 3134 |
1 files changed, 0 insertions, 3134 deletions
diff --git a/src/nbe_rewrite_head.out b/src/nbe_rewrite_head.out deleted file mode 100644 index ef9e829f3..000000000 --- a/src/nbe_rewrite_head.out +++ /dev/null @@ -1,3134 +0,0 @@ -nbe_rewrite_head = -match idc in (Compilers.ident t) return (Compile.value' true t) with -| @Literal t v => Base (##v)%expr -| Nat_succ => - fun x : expr ℕ => - ((match x with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match pattern.type.unify_extracted ℕ (projT1 args) with - | Datatypes.Some _ => - if type.type_beq base.type base.type.type_beq ℕ (projT1 args) - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base (##(Nat.succ (let (x0, _) := xv in x0)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Nat_succ)%expr @ x)%expr_pat)%option -| Nat_pred => - fun x : expr ℕ => - ((match x with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match pattern.type.unify_extracted ℕ (projT1 args) with - | Datatypes.Some _ => - if type.type_beq base.type base.type.type_beq ℕ (projT1 args) - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base (##(Nat.pred (let (x0, _) := xv in x0)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Nat_pred)%expr @ x)%expr_pat)%option -| Nat_max => - fun x x0 : expr ℕ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℕ -> ℕ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℕ -> ℕ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##(Nat.max (let (x1, _) := xv in x1) - (let (x1, _) := xv0 in x1)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Nat_max)%expr @ x @ x0)%expr_pat)%option -| Nat_mul => - fun x x0 : expr ℕ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℕ -> ℕ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℕ -> ℕ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) * - (let (x1, _) := xv0 in x1))%nat)%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Nat_mul)%expr @ x @ x0)%expr_pat)%option -| Nat_add => - fun x x0 : expr ℕ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℕ -> ℕ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℕ -> ℕ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) + - (let (x1, _) := xv0 in x1))%nat)%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Nat_add)%expr @ x @ x0)%expr_pat)%option -| Nat_sub => - fun x x0 : expr ℕ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℕ -> ℕ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℕ -> ℕ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) - - (let (x1, _) := xv0 in x1))%nat)%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Nat_sub)%expr @ x @ x0)%expr_pat)%option -| Nat_eqb => - fun x x0 : expr ℕ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℕ -> ℕ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℕ -> ℕ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) =? - (let (x1, _) := xv0 in x1))%nat)%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Nat_eqb)%expr @ x @ x0)%expr_pat)%option -| @nil t => Base []%expr_pat -| @cons t => fun (x : expr t) (x0 : expr (list t)) => Base (x :: x0)%expr_pat -| @pair A B => fun (x : expr A) (x0 : expr B) => Base (x, x0)%expr_pat -| @fst A B => - fun x : expr (A * B)%etype => - ((match x with - | @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x1) _ => - args <- invert_bind_args idc Raw.ident.pair; - match - pattern.type.unify_extracted - ((('1 * '2)%pbtype -> '1%pbtype) -> - (('1%pbtype -> '2%pbtype -> ('1 * '2)%pbtype) -> '1%pbtype) -> - '2%pbtype)%ptype - (((A * B)%etype -> A) -> - (((let (x2, _) := args in x2) -> - (let (_, y) := args in y) -> - ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) -> - s0) -> s)%ptype - with - | Datatypes.Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange => - if - type.type_beq base.type base.type.type_beq - (((b3 * b2)%etype -> b3) -> - ((b3 -> b2 -> (b3 * b2)%etype) -> b3) -> b2)%ptype - (((A * B)%etype -> A) -> - (((let (x2, _) := args in x2) -> - (let (_, y) := args in y) -> - ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) -> - s0) -> s)%ptype - then - _ <- ident.unify pattern.ident.fst fst; - _ <- ident.unify pattern.ident.pair pair; - v <- type.try_make_transport_cps s0 b3; - _ <- type.try_make_transport_cps s b2; - v1 <- base.try_make_transport_cps b3 b3; - _ <- base.try_make_transport_cps b2 b2; - v3 <- base.try_make_transport_cps b3 A; - v4 <- base.try_make_transport_cps A A; - Datatypes.Some - (fv1 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - ($(v1 (v (Compile.reflect x1)))); - Base (v4 (v3 fv1)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App - _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | - @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | - @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ => - Datatypes.None - | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr - _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s - _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(fst)%expr @ x)%expr_pat)%option -| @snd A B => - fun x : expr (A * B)%etype => - ((match x with - | @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) _) x0 => - args <- invert_bind_args idc Raw.ident.pair; - match - pattern.type.unify_extracted - ((('1 * '2)%pbtype -> '2%pbtype) -> - (('1%pbtype -> '2%pbtype -> ('1 * '2)%pbtype) -> '1%pbtype) -> - '2%pbtype)%ptype - (((A * B)%etype -> B) -> - (((let (x2, _) := args in x2) -> - (let (_, y) := args in y) -> - ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) -> - s0) -> s)%ptype - with - | Datatypes.Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange => - if - type.type_beq base.type base.type.type_beq - (((b3 * b2)%etype -> b2) -> - ((b3 -> b2 -> (b3 * b2)%etype) -> b3) -> b2)%ptype - (((A * B)%etype -> B) -> - (((let (x2, _) := args in x2) -> - (let (_, y) := args in y) -> - ((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) -> - s0) -> s)%ptype - then - _ <- ident.unify pattern.ident.snd snd; - _ <- ident.unify pattern.ident.pair pair; - _ <- type.try_make_transport_cps s0 b3; - v0 <- type.try_make_transport_cps s b2; - _ <- base.try_make_transport_cps b3 b3; - v2 <- base.try_make_transport_cps b2 b2; - v3 <- base.try_make_transport_cps b2 B; - v4 <- base.try_make_transport_cps B B; - Datatypes.Some - (fv1 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - ($(v2 (v0 (Compile.reflect x0)))); - Base (v4 (v3 fv1)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App - _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | - @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | - @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ => - Datatypes.None - | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr - _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s - _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(snd)%expr @ x)%expr_pat)%option -| @prod_rect A B T => - fun (x : expr A -> expr B -> UnderLets (expr T)) - (x0 : expr (A * B)%etype) => - ((match x0 with - | @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x2) x1 => - args <- invert_bind_args idc Raw.ident.pair; - match - pattern.type.unify_extracted - (((('1%pbtype -> '2%pbtype -> '3%pbtype) -> - ('1 * '2)%pbtype -> '3%pbtype) -> - '1%pbtype -> '2%pbtype -> '3%pbtype) -> - (('1%pbtype -> '2%pbtype -> ('1 * '2)%pbtype) -> '1%pbtype) -> - '2%pbtype)%ptype - ((((A -> B -> T) -> (A * B)%etype -> T) -> A -> B -> T) -> - (((let (x3, _) := args in x3) -> - (let (_, y) := args in y) -> - ((let (x3, _) := args in x3) * (let (_, y) := args in y))%etype) -> - s0) -> s)%ptype - with - | Datatypes.Some - (_, (_, _), (_, _, _), (_, (_, b7)), (_, (_, (_, _)), b9, b8))%zrange => - if - type.type_beq base.type base.type.type_beq - ((((b9 -> b8 -> b7) -> (b9 * b8)%etype -> b7) -> - b9 -> b8 -> b7) -> - ((b9 -> b8 -> (b9 * b8)%etype) -> b9) -> b8)%ptype - ((((A -> B -> T) -> (A * B)%etype -> T) -> A -> B -> T) -> - (((let (x3, _) := args in x3) -> - (let (_, y) := args in y) -> - ((let (x3, _) := args in x3) * (let (_, y) := args in y))%etype) -> - s0) -> s)%ptype - then - _ <- ident.unify pattern.ident.prod_rect prod_rect; - x' <- base.try_make_transport_cps A b9; - x'0 <- base.try_make_transport_cps B b8; - x'1 <- base.try_make_transport_cps T b7; - _ <- ident.unify pattern.ident.pair pair; - v <- type.try_make_transport_cps s0 b9; - v0 <- type.try_make_transport_cps s b8; - x'2 <- base.try_make_transport_cps b9 b9; - x'3 <- base.try_make_transport_cps b8 b8; - x'4 <- base.try_make_transport_cps b7 b7; - v1 <- base.try_make_transport_cps b9 b9; - v2 <- base.try_make_transport_cps b8 b8; - v3 <- base.try_make_transport_cps b7 T; - v4 <- base.try_make_transport_cps T T; - Datatypes.Some - (fv1 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - (($(x'4 (x'3 (x'2 (x'1 (x'0 (x' x)))))))%expr @ - ($(v1 (v (Compile.reflect x2))))%expr @ - ($(v2 (v0 (Compile.reflect x1))))%expr)%expr_pat; - Base (v4 (v3 fv1)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App - _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | - @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | - @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ => - Datatypes.None - | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr - _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s - _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base - (#(prod_rect)%expr @ - (λ (x1 : var A)(x2 : var B), - to_expr (x ($x1) ($x2)))%expr @ x0)%expr_pat)%option -| @bool_rect T => - fun (x x0 : expr unit -> UnderLets (expr T)) (x1 : expr bool) => - ((match x1 with - | @expr.Ident _ _ _ t idc => - (args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted - (((((unit -> '1%pbtype) -> - (unit -> '1%pbtype) -> bool -> '1%pbtype) -> - unit -> '1%pbtype) -> unit -> '1%pbtype) -> bool)%ptype - (((((unit -> T) -> (unit -> T) -> bool -> T) -> unit -> T) -> - unit -> T) -> (projT1 args))%ptype - with - | Datatypes.Some - (_, _, (_, _, (_, _)), (_, _), (_, b8), _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((((unit -> b8) -> (unit -> b8) -> bool -> b8) -> - unit -> b8) -> unit -> b8) -> bool)%ptype - (((((unit -> T) -> (unit -> T) -> bool -> T) -> unit -> T) -> - unit -> T) -> (projT1 args))%ptype - then - _ <- ident.unify pattern.ident.bool_rect bool_rect; - x' <- base.try_make_transport_cps T b8; - _ <- base.try_make_transport_cps T b8; - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - x'1 <- base.try_make_transport_cps b8 b8; - _ <- base.try_make_transport_cps b8 b8; - v <- base.try_make_transport_cps b8 T; - v0 <- base.try_make_transport_cps T T; - fv0 <- (if let (x2, _) := xv in x2 - then - Datatypes.Some - (Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - (($(x'1 (x' x)))%expr @ (##tt)%expr)%expr_pat) - else Datatypes.None); - Datatypes.Some (fv1 <-- fv0; - Base (v0 (v fv1)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end);; - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted - (((((unit -> '1%pbtype) -> - (unit -> '1%pbtype) -> bool -> '1%pbtype) -> - unit -> '1%pbtype) -> unit -> '1%pbtype) -> bool)%ptype - (((((unit -> T) -> (unit -> T) -> bool -> T) -> unit -> T) -> - unit -> T) -> (projT1 args))%ptype - with - | Datatypes.Some - (_, _, (_, _, (_, _)), (_, _), (_, b8), _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((((unit -> b8) -> (unit -> b8) -> bool -> b8) -> - unit -> b8) -> unit -> b8) -> bool)%ptype - (((((unit -> T) -> (unit -> T) -> bool -> T) -> unit -> T) -> - unit -> T) -> (projT1 args))%ptype - then - _ <- ident.unify pattern.ident.bool_rect bool_rect; - _ <- base.try_make_transport_cps T b8; - x'0 <- base.try_make_transport_cps T b8; - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - _ <- base.try_make_transport_cps b8 b8; - x'2 <- base.try_make_transport_cps b8 b8; - v <- base.try_make_transport_cps b8 T; - v0 <- base.try_make_transport_cps T T; - fv0 <- (if let (x2, _) := xv in x2 - then Datatypes.None - else - Datatypes.Some - (Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - (($(x'2 (x'0 x0)))%expr @ (##tt)%expr)%expr_pat)); - Datatypes.Some (fv1 <-- fv0; - Base (v0 (v fv1)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base - (#(bool_rect)%expr @ (λ x2 : var unit, - to_expr (x ($x2)))%expr @ - (λ x2 : var unit, - to_expr (x0 ($x2)))%expr @ x1)%expr_pat)%option -| @nat_rect P => - fun (x : expr unit -> UnderLets (expr P)) - (x0 : expr ℕ -> expr P -> UnderLets (expr P)) (x1 : expr ℕ) => - ((match x1 with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted - (((((unit -> '1%pbtype) -> - (ℕ -> '1%pbtype -> '1%pbtype) -> ℕ -> '1%pbtype) -> - unit -> '1%pbtype) -> ℕ -> '1%pbtype -> '1%pbtype) -> ℕ)%ptype - (((((unit -> P) -> (ℕ -> P -> P) -> ℕ -> P) -> unit -> P) -> - ℕ -> P -> P) -> (projT1 args))%ptype - with - | Datatypes.Some - (_, _, (_, (_, _), (_, _)), (_, _), (_, (_, b10)), _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((((unit -> b10) -> (ℕ -> b10 -> b10) -> ℕ -> b10) -> - unit -> b10) -> ℕ -> b10 -> b10) -> ℕ)%ptype - (((((unit -> P) -> (ℕ -> P -> P) -> ℕ -> P) -> unit -> P) -> - ℕ -> P -> P) -> (projT1 args))%ptype - then - _ <- ident.unify pattern.ident.nat_rect nat_rect; - x' <- base.try_make_transport_cps P b10; - x'0 <- base.try_make_transport_cps P b10; - x'1 <- base.try_make_transport_cps P b10; - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - x'2 <- base.try_make_transport_cps b10 b10; - x'3 <- base.try_make_transport_cps b10 b10; - x'4 <- base.try_make_transport_cps b10 b10; - v <- base.try_make_transport_cps b10 P; - v0 <- base.try_make_transport_cps P P; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - (#(eager_nat_rect)%expr @ ($(x'2 (x' x)))%expr @ - ($(x'4 (x'3 (x'1 (x'0 x0)))))%expr @ - (##(let (x2, _) := xv in x2))%expr)%expr_pat; - Base (v0 (v fv0)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base - (#(nat_rect)%expr @ (λ x2 : var unit, - to_expr (x ($x2)))%expr @ - (λ (x2 : var ℕ)(x3 : var P), - to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat)%option -| @nat_rect_arrow P Q => - fun (x : expr P -> UnderLets (expr Q)) - (x0 : expr ℕ -> - (expr P -> UnderLets (expr Q)) -> expr P -> UnderLets (expr Q)) - (x1 : expr ℕ) (x2 : expr P) => - (match x1 with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted - (((((('1%pbtype -> '2%pbtype) -> - (ℕ -> ('1%pbtype -> '2%pbtype) -> '1%pbtype -> '2%pbtype) -> - ℕ -> '1%pbtype -> '2%pbtype) -> '1%pbtype -> '2%pbtype) -> - ℕ -> ('1%pbtype -> '2%pbtype) -> '1%pbtype -> '2%pbtype) -> ℕ) -> - '1%pbtype)%ptype - ((((((P -> Q) -> (ℕ -> (P -> Q) -> P -> Q) -> ℕ -> P -> Q) -> - P -> Q) -> ℕ -> (P -> Q) -> P -> Q) -> (projT1 args)) -> P)%ptype - with - | Datatypes.Some - (_, _, (_, (_, _, (_, _)), (_, (_, _))), (_, _), - (_, (_, _, (_, b16))), _, b)%zrange => - if - type.type_beq base.type base.type.type_beq - ((((((b -> b16) -> - (ℕ -> (b -> b16) -> b -> b16) -> ℕ -> b -> b16) -> - b -> b16) -> ℕ -> (b -> b16) -> b -> b16) -> ℕ) -> b)%ptype - ((((((P -> Q) -> (ℕ -> (P -> Q) -> P -> Q) -> ℕ -> P -> Q) -> - P -> Q) -> ℕ -> (P -> Q) -> P -> Q) -> (projT1 args)) -> - P)%ptype - then - _ <- ident.unify pattern.ident.nat_rect_arrow nat_rect_arrow; - x' <- base.try_make_transport_cps P b; - x'0 <- base.try_make_transport_cps Q b16; - x'1 <- base.try_make_transport_cps P b; - x'2 <- base.try_make_transport_cps Q b16; - x'3 <- base.try_make_transport_cps P b; - x'4 <- base.try_make_transport_cps Q b16; - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - v <- base.try_make_transport_cps P b; - x'5 <- base.try_make_transport_cps b b; - x'6 <- base.try_make_transport_cps b16 b16; - x'7 <- base.try_make_transport_cps b b; - x'8 <- base.try_make_transport_cps b16 b16; - x'9 <- base.try_make_transport_cps b b; - x'10 <- base.try_make_transport_cps b16 b16; - v0 <- base.try_make_transport_cps b b; - v1 <- base.try_make_transport_cps b16 Q; - v2 <- base.try_make_transport_cps Q Q; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - (#(eager_nat_rect_arrow)%expr @ - ($(x'6 (x'5 (x'0 (x' x)))))%expr @ - ($(x'10 - (x'9 (x'8 (x'7 (x'4 (x'3 (x'2 (x'1 x0)))))))))%expr @ - (##(let (x3, _) := xv in x3))%expr @ - ($(v0 (v x2)))%expr)%expr_pat; - Base (v2 (v1 fv0)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;;; - Base - (#(nat_rect_arrow)%expr @ (λ x3 : var P, - to_expr (x ($x3)))%expr @ - (λ (x3 : var ℕ)(x4 : var (P -> Q)%ptype)(x5 : var P), - to_expr - (x0 ($x3) (fun x6 : expr P => Base ($x4 @ x6)%expr_pat) ($x5)))%expr @ - x1 @ x2)%expr_pat)%option -| @eager_nat_rect P => - fun (x : expr unit -> UnderLets (expr P)) - (x0 : expr ℕ -> expr P -> UnderLets (expr P)) (x1 : expr ℕ) => - Base - (#(eager_nat_rect)%expr @ (λ x2 : var unit, - to_expr (x ($x2)))%expr @ - (λ (x2 : var ℕ)(x3 : var P), - to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat -| @eager_nat_rect_arrow P Q => - fun (x : expr P -> UnderLets (expr Q)) - (x0 : expr ℕ -> - (expr P -> UnderLets (expr Q)) -> expr P -> UnderLets (expr Q)) - (x1 : expr ℕ) (x2 : expr P) => - Base - (#(eager_nat_rect_arrow)%expr @ (λ x3 : var P, - to_expr (x ($x3)))%expr @ - (λ (x3 : var ℕ)(x4 : var (P -> Q)%ptype)(x5 : var P), - to_expr - (x0 ($x3) (fun x6 : expr P => Base ($x4 @ x6)%expr_pat) ($x5)))%expr @ - x1 @ x2)%expr_pat -| @list_rect A P => - fun (x : expr unit -> UnderLets (expr P)) - (x0 : expr A -> expr (list A) -> expr P -> UnderLets (expr P)) - (x1 : expr (list A)) => - ((match - pattern.type.unify_extracted - (((((unit -> '2%pbtype) -> - ('1%pbtype -> - (pattern.base.type.list '1) -> '2%pbtype -> '2%pbtype) -> - (pattern.base.type.list '1) -> '2%pbtype) -> unit -> '2%pbtype) -> - '1%pbtype -> - (pattern.base.type.list '1) -> '2%pbtype -> '2%pbtype) -> - (pattern.base.type.list '1))%ptype - (((((unit -> P) -> (A -> (list A) -> P -> P) -> (list A) -> P) -> - unit -> P) -> A -> (list A) -> P -> P) -> (list A))%ptype - with - | Datatypes.Some - (_, _, (_, (_, (_, _)), (_, _)), (_, _), (_, (_, (_, b12))), b)%zrange => - if - type.type_beq base.type base.type.type_beq - (((((unit -> b12) -> - (b -> (list b) -> b12 -> b12) -> (list b) -> b12) -> - unit -> b12) -> b -> (list b) -> b12 -> b12) -> (list b))%ptype - (((((unit -> P) -> (A -> (list A) -> P -> P) -> (list A) -> P) -> - unit -> P) -> A -> (list A) -> P -> P) -> (list A))%ptype - then - _ <- ident.unify pattern.ident.list_rect list_rect; - x' <- base.try_make_transport_cps P b12; - x'0 <- base.try_make_transport_cps A b; - x'1 <- base.try_make_transport_cps A b; - x'2 <- base.try_make_transport_cps P b12; - x'3 <- base.try_make_transport_cps P b12; - v <- base.try_make_transport_cps A b; - x'4 <- base.try_make_transport_cps b12 b12; - x'5 <- base.try_make_transport_cps b b; - x'6 <- base.try_make_transport_cps b b; - x'7 <- base.try_make_transport_cps b12 b12; - x'8 <- base.try_make_transport_cps b12 b12; - v0 <- base.try_make_transport_cps b b; - v1 <- base.try_make_transport_cps b12 P; - v2 <- base.try_make_transport_cps P P; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - (#(eager_list_rect)%expr @ ($(x'4 (x' x)))%expr @ - ($(x'8 (x'7 (x'6 (x'5 (x'3 (x'2 (x'1 (x'0 x0)))))))))%expr @ - ($(v0 (v x1)))%expr)%expr_pat; - Base (v2 (v1 fv0)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end;; - Datatypes.None);;; - Base - (#(list_rect)%expr @ (λ x2 : var unit, - to_expr (x ($x2)))%expr @ - (λ (x2 : var A)(x3 : var (list A))(x4 : var P), - to_expr (x0 ($x2) ($x3) ($x4)))%expr @ x1)%expr_pat)%option -| @list_rect_arrow A P Q => - fun (x : expr P -> UnderLets (expr Q)) - (x0 : expr A -> - expr (list A) -> - (expr P -> UnderLets (expr Q)) -> expr P -> UnderLets (expr Q)) - (x1 : expr (list A)) (x2 : expr P) => - ((match - pattern.type.unify_extracted - (((((('2%pbtype -> '3%pbtype) -> - ('1%pbtype -> - (pattern.base.type.list '1) -> - ('2%pbtype -> '3%pbtype) -> '2%pbtype -> '3%pbtype) -> - (pattern.base.type.list '1) -> '2%pbtype -> '3%pbtype) -> - '2%pbtype -> '3%pbtype) -> - '1%pbtype -> - (pattern.base.type.list '1) -> - ('2%pbtype -> '3%pbtype) -> '2%pbtype -> '3%pbtype) -> - (pattern.base.type.list '1)) -> '2%pbtype)%ptype - ((((((P -> Q) -> - (A -> (list A) -> (P -> Q) -> P -> Q) -> (list A) -> P -> Q) -> - P -> Q) -> A -> (list A) -> (P -> Q) -> P -> Q) -> (list A)) -> - P)%ptype - with - | Datatypes.Some - (_, _, (_, (_, (_, _, (_, _))), (_, (_, _))), (_, _), - (_, (_, (_, _, (_, b18)))), b0, b)%zrange => - if - type.type_beq base.type base.type.type_beq - ((((((b -> b18) -> - (b0 -> (list b0) -> (b -> b18) -> b -> b18) -> - (list b0) -> b -> b18) -> b -> b18) -> - b0 -> (list b0) -> (b -> b18) -> b -> b18) -> (list b0)) -> b)%ptype - ((((((P -> Q) -> - (A -> (list A) -> (P -> Q) -> P -> Q) -> (list A) -> P -> Q) -> - P -> Q) -> A -> (list A) -> (P -> Q) -> P -> Q) -> (list A)) -> - P)%ptype - then - _ <- ident.unify pattern.ident.list_rect_arrow list_rect_arrow; - x' <- base.try_make_transport_cps P b; - x'0 <- base.try_make_transport_cps Q b18; - x'1 <- base.try_make_transport_cps A b0; - x'2 <- base.try_make_transport_cps A b0; - x'3 <- base.try_make_transport_cps P b; - x'4 <- base.try_make_transport_cps Q b18; - x'5 <- base.try_make_transport_cps P b; - x'6 <- base.try_make_transport_cps Q b18; - v <- base.try_make_transport_cps A b0; - v0 <- base.try_make_transport_cps P b; - x'7 <- base.try_make_transport_cps b b; - x'8 <- base.try_make_transport_cps b18 b18; - x'9 <- base.try_make_transport_cps b0 b0; - x'10 <- base.try_make_transport_cps b0 b0; - x'11 <- base.try_make_transport_cps b b; - x'12 <- base.try_make_transport_cps b18 b18; - x'13 <- base.try_make_transport_cps b b; - x'14 <- base.try_make_transport_cps b18 b18; - v1 <- base.try_make_transport_cps b0 b0; - v2 <- base.try_make_transport_cps b b; - v3 <- base.try_make_transport_cps b18 Q; - v4 <- base.try_make_transport_cps Q Q; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - (#(eager_list_rect_arrow)%expr @ - ($(x'8 (x'7 (x'0 (x' x)))))%expr @ - ($(x'14 - (x'13 - (x'12 - (x'11 - (x'10 - (x'9 - (x'6 - (x'5 - (x'4 (x'3 (x'2 (x'1 x0)))))))))))))%expr @ - ($(v1 (v x1)))%expr @ ($(v2 (v0 x2)))%expr)%expr_pat; - Base (v4 (v3 fv0)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end;; - Datatypes.None);;; - Base - (#(list_rect_arrow)%expr @ (λ x3 : var P, - to_expr (x ($x3)))%expr @ - (λ (x3 : var A)(x4 : var (list A))(x5 : var (P -> Q)%ptype)(x6 : - var P), - to_expr - (x0 ($x3) ($x4) (fun x7 : expr P => Base ($x5 @ x7)%expr_pat) - ($x6)))%expr @ x1 @ x2)%expr_pat)%option -| @eager_list_rect A P => - fun (x : expr unit -> UnderLets (expr P)) - (x0 : expr A -> expr (list A) -> expr P -> UnderLets (expr P)) - (x1 : expr (list A)) => - Base - (#(eager_list_rect)%expr @ (λ x2 : var unit, - to_expr (x ($x2)))%expr @ - (λ (x2 : var A)(x3 : var (list A))(x4 : var P), - to_expr (x0 ($x2) ($x3) ($x4)))%expr @ x1)%expr_pat -| @eager_list_rect_arrow A P Q => - fun (x : expr P -> UnderLets (expr Q)) - (x0 : expr A -> - expr (list A) -> - (expr P -> UnderLets (expr Q)) -> expr P -> UnderLets (expr Q)) - (x1 : expr (list A)) (x2 : expr P) => - Base - (#(eager_list_rect_arrow)%expr @ (λ x3 : var P, - to_expr (x ($x3)))%expr @ - (λ (x3 : var A)(x4 : var (list A))(x5 : var (P -> Q)%ptype)(x6 : - var P), - to_expr - (x0 ($x3) ($x4) (fun x7 : expr P => Base ($x5 @ x7)%expr_pat) ($x6)))%expr @ - x1 @ x2)%expr_pat -| @list_case A P => - fun (x : expr unit -> UnderLets (expr P)) - (x0 : expr A -> expr (list A) -> UnderLets (expr P)) - (x1 : expr (list A)) => - ((match x1 with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.nil; - match - pattern.type.unify_extracted - (((((unit -> '2%pbtype) -> - ('1%pbtype -> (pattern.base.type.list '1) -> '2%pbtype) -> - (pattern.base.type.list '1) -> '2%pbtype) -> - unit -> '2%pbtype) -> - '1%pbtype -> (pattern.base.type.list '1) -> '2%pbtype) -> - (pattern.base.type.list '1))%ptype - (((((unit -> P) -> (A -> (list A) -> P) -> (list A) -> P) -> - unit -> P) -> A -> (list A) -> P) -> (list args))%ptype - with - | Datatypes.Some - (_, _, (_, (_, _), (_, _)), (_, _), (_, (_, b10)), b)%zrange => - if - type.type_beq base.type base.type.type_beq - (((((unit -> b10) -> - (b -> (list b) -> b10) -> (list b) -> b10) -> - unit -> b10) -> b -> (list b) -> b10) -> (list b))%ptype - (((((unit -> P) -> (A -> (list A) -> P) -> (list A) -> P) -> - unit -> P) -> A -> (list A) -> P) -> (list args))%ptype - then - _ <- ident.unify pattern.ident.list_case list_case; - x' <- base.try_make_transport_cps P b10; - _ <- base.try_make_transport_cps A b; - _ <- base.try_make_transport_cps A b; - _ <- base.try_make_transport_cps P b10; - _ <- ident.unify pattern.ident.nil nil; - x'3 <- base.try_make_transport_cps b10 b10; - _ <- base.try_make_transport_cps b b; - _ <- base.try_make_transport_cps b b; - _ <- base.try_make_transport_cps b10 b10; - v <- base.try_make_transport_cps b10 P; - v0 <- base.try_make_transport_cps P P; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - (($(x'3 (x' x)))%expr @ (##tt)%expr)%expr_pat; - Base (v0 (v fv0)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x3) x2 => - args <- invert_bind_args idc Raw.ident.cons; - match - pattern.type.unify_extracted - (((((unit -> '2%pbtype) -> - ('1%pbtype -> (pattern.base.type.list '1) -> '2%pbtype) -> - (pattern.base.type.list '1) -> '2%pbtype) -> - unit -> '2%pbtype) -> - '1%pbtype -> (pattern.base.type.list '1) -> '2%pbtype) -> - (('1%pbtype -> - (pattern.base.type.list '1) -> (pattern.base.type.list '1)) -> - '1%pbtype) -> (pattern.base.type.list '1))%ptype - (((((unit -> P) -> (A -> (list A) -> P) -> (list A) -> P) -> - unit -> P) -> A -> (list A) -> P) -> - ((args -> (list args) -> (list args)) -> s0) -> s)%ptype - with - | Datatypes.Some - (_, _, (_, (_, _), (_, _)), (_, _), (_, (_, b10)), - (_, (_, _), _, b11))%zrange => - if - type.type_beq base.type base.type.type_beq - (((((unit -> b10) -> - (b11 -> (list b11) -> b10) -> (list b11) -> b10) -> - unit -> b10) -> b11 -> (list b11) -> b10) -> - ((b11 -> (list b11) -> (list b11)) -> b11) -> (list b11))%ptype - (((((unit -> P) -> (A -> (list A) -> P) -> (list A) -> P) -> - unit -> P) -> A -> (list A) -> P) -> - ((args -> (list args) -> (list args)) -> s0) -> s)%ptype - then - _ <- ident.unify pattern.ident.list_case list_case; - _ <- base.try_make_transport_cps P b10; - x'0 <- base.try_make_transport_cps A b11; - x'1 <- base.try_make_transport_cps A b11; - x'2 <- base.try_make_transport_cps P b10; - _ <- ident.unify pattern.ident.cons cons; - v <- type.try_make_transport_cps s0 b11; - v0 <- type.try_make_transport_cps s (list b11); - _ <- base.try_make_transport_cps b10 b10; - x'4 <- base.try_make_transport_cps b11 b11; - x'5 <- base.try_make_transport_cps b11 b11; - x'6 <- base.try_make_transport_cps b10 b10; - v1 <- base.try_make_transport_cps b11 b11; - v2 <- base.try_make_transport_cps b11 b11; - v3 <- base.try_make_transport_cps b10 P; - v4 <- base.try_make_transport_cps P P; - Datatypes.Some - (fv1 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - (($(x'6 (x'5 (x'4 (x'2 (x'1 (x'0 x0)))))))%expr @ - ($(v1 (v (Compile.reflect x3))))%expr @ - ($(v2 (v0 (Compile.reflect x2))))%expr)%expr_pat; - Base (v4 (v3 fv1)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App - _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | - @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | - @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ => - Datatypes.None - | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr - _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s - _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base - (#(list_case)%expr @ (λ x2 : var unit, - to_expr (x ($x2)))%expr @ - (λ (x2 : var A)(x3 : var (list A)), - to_expr (x0 ($x2) ($x3)))%expr @ x1)%expr_pat)%option -| @List_length T => - fun x : expr (list T) => - ((match - pattern.type.unify_extracted - (((pattern.base.type.list '1) -> ℕ) -> (pattern.base.type.list '1))%ptype - (((list T) -> ℕ) -> (list T))%ptype - with - | Datatypes.Some (_, _, b)%zrange => - if - type.type_beq base.type base.type.type_beq - (((list b) -> ℕ) -> (list b))%ptype - (((list T) -> ℕ) -> (list T))%ptype - then - _ <- ident.unify pattern.ident.List_length List_length; - v <- base.try_make_transport_cps T b; - v0 <- base.try_make_transport_cps b b; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) true - (#(list_rect)%expr @ (λ _ : expr unit, - ##0%nat)%expr @ - (λ (_ : expr b)(_ : expr (list b))(v3 : expr ℕ), - (#(Nat_succ)%expr @ $v3)%expr_pat)%expr @ - ($(v0 (v x)))%expr)%expr_pat; - fv1 <-- do_again ℕ fv0; - Base fv1)%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end;; - Datatypes.None);;; - Base (#(List_length)%expr @ x)%expr_pat)%option -| List_seq => - fun x x0 : expr ℕ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℕ -> ℕ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℕ -> ℕ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (Compilers.reify_list - (List.map (fun v : nat => (##v)%expr) - (seq (let (x1, _) := xv in x1) - (let (x1, _) := xv0 in x1))))) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(List_seq)%expr @ x @ x0)%expr_pat)%option -| @List_firstn A => - fun (x : expr ℕ) (x0 : expr (list A)) => - ((match x with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted - (((ℕ -> - (pattern.base.type.list '1) -> (pattern.base.type.list '1)) -> - ℕ) -> (pattern.base.type.list '1))%ptype - (((ℕ -> (list A) -> (list A)) -> (projT1 args)) -> (list A))%ptype - with - | Datatypes.Some (_, (_, _), _, b)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℕ -> (list b) -> (list b)) -> ℕ) -> (list b))%ptype - (((ℕ -> (list A) -> (list A)) -> (projT1 args)) -> (list A))%ptype - then - _ <- ident.unify pattern.ident.List_firstn List_firstn; - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - v <- base.try_make_transport_cps A b; - v0 <- base.try_make_transport_cps b b; - v1 <- base.try_make_transport_cps b A; - v2 <- base.try_make_transport_cps A A; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) true - (#(nat_rect_arrow)%expr @ - (λ _ : expr (list b), - []%expr_pat)%expr @ - (λ (_ : expr ℕ)(v4 : expr (list b) -> - UnderLets (expr (list b))) - (v5 : expr (list b)), - (#(list_case)%expr @ - (λ _ : expr unit, - []%expr_pat) @ - (λ (v6 : expr b)(v7 : expr (list b)), - ($v6 :: $v4 @ $v7)%expr_pat) @ $v5)%expr_pat)%expr @ - (##(let (x1, _) := xv in x1))%expr @ - ($(v0 (v x0)))%expr)%expr_pat; - fv1 <-- do_again (list A) (v1 fv0); - Base (v2 fv1))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(List_firstn)%expr @ x @ x0)%expr_pat)%option -| @List_skipn A => - fun (x : expr ℕ) (x0 : expr (list A)) => - ((match x with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted - (((ℕ -> - (pattern.base.type.list '1) -> (pattern.base.type.list '1)) -> - ℕ) -> (pattern.base.type.list '1))%ptype - (((ℕ -> (list A) -> (list A)) -> (projT1 args)) -> (list A))%ptype - with - | Datatypes.Some (_, (_, _), _, b)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℕ -> (list b) -> (list b)) -> ℕ) -> (list b))%ptype - (((ℕ -> (list A) -> (list A)) -> (projT1 args)) -> (list A))%ptype - then - _ <- ident.unify pattern.ident.List_skipn List_skipn; - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - v <- base.try_make_transport_cps A b; - v0 <- base.try_make_transport_cps b b; - v1 <- base.try_make_transport_cps b A; - v2 <- base.try_make_transport_cps A A; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) true - (#(nat_rect_arrow)%expr @ - (λ v3 : expr (list b), - $v3)%expr @ - (λ (_ : expr ℕ)(v4 : expr (list b) -> - UnderLets (expr (list b))) - (v5 : expr (list b)), - (#(list_case)%expr @ - (λ _ : expr unit, - []%expr_pat) @ - (λ (_ : expr b)(v7 : expr (list b)), - ($v4 @ $v7)%expr_pat) @ $v5)%expr_pat)%expr @ - (##(let (x1, _) := xv in x1))%expr @ - ($(v0 (v x0)))%expr)%expr_pat; - fv1 <-- do_again (list A) (v1 fv0); - Base (v2 fv1))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(List_skipn)%expr @ x @ x0)%expr_pat)%option -| @List_repeat A => - fun (x : expr A) (x0 : expr ℕ) => - ((match x0 with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted - ((('1%pbtype -> ℕ -> (pattern.base.type.list '1)) -> '1%pbtype) -> - ℕ)%ptype (((A -> ℕ -> (list A)) -> A) -> (projT1 args))%ptype - with - | Datatypes.Some (_, (_, _), b0, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((b0 -> ℕ -> (list b0)) -> b0) -> ℕ)%ptype - (((A -> ℕ -> (list A)) -> A) -> (projT1 args))%ptype - then - _ <- ident.unify pattern.ident.List_repeat List_repeat; - v <- base.try_make_transport_cps A b0; - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - v0 <- base.try_make_transport_cps b0 b0; - v1 <- base.try_make_transport_cps b0 A; - v2 <- base.try_make_transport_cps A A; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - (#(eager_nat_rect)%expr @ - (λ _ : expr unit, - []%expr_pat)%expr @ - (λ (_ : expr ℕ)(v4 : expr (list b0)), - ($(v0 (v x)) :: $v4)%expr_pat)%expr @ - (##(let (x1, _) := xv in x1))%expr)%expr_pat; - Base (v2 (v1 fv0)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(List_repeat)%expr @ x @ x0)%expr_pat)%option -| @List_combine A B => - fun (x : expr (list A)) (x0 : expr (list B)) => - ((match - pattern.type.unify_extracted - ((((pattern.base.type.list '1) -> - (pattern.base.type.list '2) -> - (pattern.base.type.list ('1 * '2))) -> - (pattern.base.type.list '1)) -> (pattern.base.type.list '2))%ptype - ((((list A) -> (list B) -> (list (A * B))) -> (list A)) -> (list B))%ptype - with - | Datatypes.Some (_, (_, (_, _)), b0, b)%zrange => - if - type.type_beq base.type base.type.type_beq - ((((list b0) -> (list b) -> (list (b0 * b))) -> (list b0)) -> - (list b))%ptype - ((((list A) -> (list B) -> (list (A * B))) -> (list A)) -> - (list B))%ptype - then - _ <- ident.unify pattern.ident.List_combine List_combine; - v <- base.try_make_transport_cps A b0; - v0 <- base.try_make_transport_cps B b; - v1 <- base.try_make_transport_cps b0 b0; - v2 <- base.try_make_transport_cps b b; - x' <- base.try_make_transport_cps b0 A; - x'0 <- base.try_make_transport_cps b B; - x'1 <- base.try_make_transport_cps A A; - x'2 <- base.try_make_transport_cps B B; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) true - (#(list_rect_arrow)%expr @ - (λ _ : expr (list b), - []%expr_pat)%expr @ - (λ (v3 : expr b0)(_ : expr (list b0))(v5 : expr - (list b) -> - UnderLets - (expr - (list - (b0 * b)))) - (v6 : expr (list b)), - (#(list_case)%expr @ (λ _ : expr unit, - []%expr_pat) @ - (λ (v7 : expr b)(v8 : expr (list b)), - (($v3, $v7) :: $v5 @ $v8)%expr_pat) @ $v6)%expr_pat)%expr @ - ($(v1 (v x)))%expr @ ($(v2 (v0 x0)))%expr)%expr_pat; - fv1 <-- do_again (list (A * B)) (x'0 (x' fv0)); - Base (x'2 (x'1 fv1)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end;; - Datatypes.None);;; - Base (#(List_combine)%expr @ x @ x0)%expr_pat)%option -| @List_map A B => - fun (x : expr A -> UnderLets (expr B)) (x0 : expr (list A)) => - ((match - pattern.type.unify_extracted - (((('1%pbtype -> '2%pbtype) -> - (pattern.base.type.list '1) -> (pattern.base.type.list '2)) -> - '1%pbtype -> '2%pbtype) -> (pattern.base.type.list '1))%ptype - ((((A -> B) -> (list A) -> (list B)) -> A -> B) -> (list A))%ptype - with - | Datatypes.Some (_, _, (_, _), (_, b4), b)%zrange => - if - type.type_beq base.type base.type.type_beq - ((((b -> b4) -> (list b) -> (list b4)) -> b -> b4) -> (list b))%ptype - ((((A -> B) -> (list A) -> (list B)) -> A -> B) -> (list A))%ptype - then - _ <- ident.unify pattern.ident.List_map List_map; - x' <- base.try_make_transport_cps A b; - x'0 <- base.try_make_transport_cps B b4; - v <- base.try_make_transport_cps A b; - x'1 <- base.try_make_transport_cps b b; - x'2 <- base.try_make_transport_cps b4 b4; - v0 <- base.try_make_transport_cps b b; - v1 <- base.try_make_transport_cps b4 B; - v2 <- base.try_make_transport_cps B B; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - (#(eager_list_rect)%expr @ - (λ _ : expr unit, - []%expr_pat)%expr @ - (λ (v3 : expr b)(_ : expr (list b))(v5 : expr - (list b4)), - ($(x'2 (x'1 (x'0 (x' x)))) @ $v3 :: $v5)%expr_pat)%expr @ - ($(v0 (v x0)))%expr)%expr_pat; - Base (v2 (v1 fv0)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end;; - Datatypes.None);;; - Base - (#(List_map)%expr @ (λ x1 : var A, - to_expr (x ($x1)))%expr @ x0)%expr_pat)%option -| @List_app A => - fun x x0 : expr (list A) => - ((match - pattern.type.unify_extracted - ((((pattern.base.type.list '1) -> - (pattern.base.type.list '1) -> (pattern.base.type.list '1)) -> - (pattern.base.type.list '1)) -> (pattern.base.type.list '1))%ptype - ((((list A) -> (list A) -> (list A)) -> (list A)) -> (list A))%ptype - with - | Datatypes.Some (_, (_, _), _, b)%zrange => - if - type.type_beq base.type base.type.type_beq - ((((list b) -> (list b) -> (list b)) -> (list b)) -> (list b))%ptype - ((((list A) -> (list A) -> (list A)) -> (list A)) -> (list A))%ptype - then - _ <- ident.unify pattern.ident.List_app List_app; - v <- base.try_make_transport_cps A b; - v0 <- base.try_make_transport_cps A b; - v1 <- base.try_make_transport_cps b b; - v2 <- base.try_make_transport_cps b b; - v3 <- base.try_make_transport_cps b A; - v4 <- base.try_make_transport_cps A A; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - (#(eager_list_rect)%expr @ - (λ _ : expr unit, - $(v2 (v0 x0)))%expr @ - (λ (v5 : expr b)(_ v7 : expr (list b)), - ($v5 :: $v7)%expr_pat)%expr @ ($(v1 (v x)))%expr)%expr_pat; - Base (v4 (v3 fv0)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end;; - Datatypes.None);;; - Base (x ++ x0)%expr)%option -| @List_rev A => - fun x : expr (list A) => - (match - pattern.type.unify_extracted - (((pattern.base.type.list '1) -> (pattern.base.type.list '1)) -> - (pattern.base.type.list '1))%ptype - (((list A) -> (list A)) -> (list A))%ptype - with - | Datatypes.Some (_, _, b)%zrange => - if - type.type_beq base.type base.type.type_beq - (((list b) -> (list b)) -> (list b))%ptype - (((list A) -> (list A)) -> (list A))%ptype - then - _ <- ident.unify pattern.ident.List_rev List_rev; - v <- base.try_make_transport_cps A b; - v0 <- base.try_make_transport_cps b b; - v1 <- base.try_make_transport_cps b A; - v2 <- base.try_make_transport_cps A A; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) true - (#(list_rect)%expr @ - (λ _ : expr unit, - []%expr_pat)%expr @ - (λ (v3 : expr b)(_ v5 : expr (list b)), - $v5 ++ [$v3])%expr @ ($(v0 (v x)))%expr)%expr_pat; - fv1 <-- do_again (list A) (v1 fv0); - Base (v2 fv1))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end;;; - Base (#(List_rev)%expr @ x)%expr_pat)%option -| @List_flat_map A B => - fun (x : expr A -> UnderLets (expr (list B))) (x0 : expr (list A)) => - ((match - pattern.type.unify_extracted - (((('1%pbtype -> (pattern.base.type.list '2)) -> - (pattern.base.type.list '1) -> (pattern.base.type.list '2)) -> - '1%pbtype -> (pattern.base.type.list '2)) -> - (pattern.base.type.list '1))%ptype - ((((A -> (list B)) -> (list A) -> (list B)) -> A -> (list B)) -> - (list A))%ptype - with - | Datatypes.Some (_, _, (_, _), (_, b4), b)%zrange => - if - type.type_beq base.type base.type.type_beq - ((((b -> (list b4)) -> (list b) -> (list b4)) -> b -> (list b4)) -> - (list b))%ptype - ((((A -> (list B)) -> (list A) -> (list B)) -> A -> (list B)) -> - (list A))%ptype - then - _ <- ident.unify pattern.ident.List_flat_map List_flat_map; - x' <- base.try_make_transport_cps A b; - x'0 <- base.try_make_transport_cps B b4; - v <- base.try_make_transport_cps A b; - x'1 <- base.try_make_transport_cps b b; - x'2 <- base.try_make_transport_cps b4 b4; - v0 <- base.try_make_transport_cps b b; - v1 <- base.try_make_transport_cps b4 B; - v2 <- base.try_make_transport_cps B B; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) true - (#(list_rect)%expr @ - (λ _ : expr unit, - []%expr_pat)%expr @ - (λ (v3 : expr b)(_ : expr (list b))(v5 : expr - (list b4)), - ($(x'2 (x'1 (x'0 (x' x)))) @ $v3)%expr_pat ++ $v5)%expr @ - ($(v0 (v x0)))%expr)%expr_pat; - fv1 <-- do_again (list B) (v1 fv0); - Base (v2 fv1))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end;; - Datatypes.None);;; - Base - (#(List_flat_map)%expr @ (λ x1 : var A, - to_expr (x ($x1)))%expr @ x0)%expr_pat)%option -| @List_partition A => - fun (x : expr A -> UnderLets (expr bool)) (x0 : expr (list A)) => - (match - pattern.type.unify_extracted - (((('1%pbtype -> bool) -> - (pattern.base.type.list '1) -> - (pattern.base.type.list '1 * pattern.base.type.list '1)%pbtype) -> - '1%pbtype -> bool) -> (pattern.base.type.list '1))%ptype - ((((A -> bool) -> (list A) -> (list A * list A)%etype) -> A -> bool) -> - (list A))%ptype - with - | Datatypes.Some (_, _, (_, (_, _)), (_, _), b)%zrange => - if - type.type_beq base.type base.type.type_beq - ((((b -> bool) -> (list b) -> (list b * list b)%etype) -> - b -> bool) -> (list b))%ptype - ((((A -> bool) -> (list A) -> (list A * list A)%etype) -> - A -> bool) -> (list A))%ptype - then - _ <- ident.unify pattern.ident.List_partition List_partition; - x' <- base.try_make_transport_cps A b; - v <- base.try_make_transport_cps A b; - x'0 <- base.try_make_transport_cps b b; - v0 <- base.try_make_transport_cps b b; - x'1 <- base.try_make_transport_cps b A; - x'2 <- base.try_make_transport_cps b A; - x'3 <- base.try_make_transport_cps A A; - x'4 <- base.try_make_transport_cps A A; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) true - (#(list_rect)%expr @ - (λ _ : expr unit, - ([], [])%expr_pat)%expr @ - (λ (v1 : expr b)(_ : expr (list b))(v3 : expr - (list b * - list b)%etype), - (#(prod_rect)%expr @ - (λ v4 v5 : expr (list b), - (#(bool_rect)%expr @ - (λ _ : expr unit, - ($v1 :: $v4, $v5)%expr_pat) @ - (λ _ : expr unit, - ($v4, $v1 :: $v5)%expr_pat) @ - ($(x'0 (x' x)) @ $v1))%expr_pat) @ $v3)%expr_pat)%expr @ - ($(v0 (v x0)))%expr)%expr_pat; - fv1 <-- do_again (list A * list A) (x'2 (x'1 fv0)); - Base (x'4 (x'3 fv1)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end;;; - Base - (#(List_partition)%expr @ (λ x1 : var A, - to_expr (x ($x1)))%expr @ x0)%expr_pat)%option -| @List_fold_right A B => - fun (x : expr B -> expr A -> UnderLets (expr A)) (x0 : expr A) - (x1 : expr (list B)) => - ((match - pattern.type.unify_extracted - ((((('2%pbtype -> '1%pbtype -> '1%pbtype) -> - '1%pbtype -> (pattern.base.type.list '2) -> '1%pbtype) -> - '2%pbtype -> '1%pbtype -> '1%pbtype) -> '1%pbtype) -> - (pattern.base.type.list '2))%ptype - (((((B -> A -> A) -> A -> (list B) -> A) -> B -> A -> A) -> A) -> - (list B))%ptype - with - | Datatypes.Some (_, (_, _), (_, (_, _)), (_, (_, _)), b0, b)%zrange => - if - type.type_beq base.type base.type.type_beq - (((((b -> b0 -> b0) -> b0 -> (list b) -> b0) -> b -> b0 -> b0) -> - b0) -> (list b))%ptype - (((((B -> A -> A) -> A -> (list B) -> A) -> B -> A -> A) -> A) -> - (list B))%ptype - then - _ <- ident.unify pattern.ident.List_fold_right List_fold_right; - x' <- base.try_make_transport_cps B b; - x'0 <- base.try_make_transport_cps A b0; - x'1 <- base.try_make_transport_cps A b0; - v <- base.try_make_transport_cps A b0; - v0 <- base.try_make_transport_cps B b; - x'2 <- base.try_make_transport_cps b b; - x'3 <- base.try_make_transport_cps b0 b0; - x'4 <- base.try_make_transport_cps b0 b0; - v1 <- base.try_make_transport_cps b0 b0; - v2 <- base.try_make_transport_cps b b; - v3 <- base.try_make_transport_cps b0 A; - v4 <- base.try_make_transport_cps A A; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - (#(eager_list_rect)%expr @ - (λ _ : expr unit, - $(v1 (v x0)))%expr @ - (λ (v5 : expr b)(_ : expr (list b))(v7 : expr b0), - ($(x'4 (x'3 (x'2 (x'1 (x'0 (x' x)))))) @ $v5 @ $v7)%expr_pat)%expr @ - ($(v2 (v0 x1)))%expr)%expr_pat; - Base (v4 (v3 fv0)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end;; - Datatypes.None);;; - Base - (#(List_fold_right)%expr @ - (λ (x2 : var B)(x3 : var A), - to_expr (x ($x2) ($x3)))%expr @ x0 @ x1)%expr_pat)%option -| @List_update_nth T => - fun (x : expr ℕ) (x0 : expr T -> UnderLets (expr T)) (x1 : expr (list T)) - => - (match x with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted - ((((ℕ -> - ('1%pbtype -> '1%pbtype) -> - (pattern.base.type.list '1) -> (pattern.base.type.list '1)) -> - ℕ) -> '1%pbtype -> '1%pbtype) -> (pattern.base.type.list '1))%ptype - ((((ℕ -> (T -> T) -> (list T) -> (list T)) -> (projT1 args)) -> - T -> T) -> (list T))%ptype - with - | Datatypes.Some (_, (_, _, (_, _)), _, (_, _), b)%zrange => - if - type.type_beq base.type base.type.type_beq - ((((ℕ -> (b -> b) -> (list b) -> (list b)) -> ℕ) -> b -> b) -> - (list b))%ptype - ((((ℕ -> (T -> T) -> (list T) -> (list T)) -> (projT1 args)) -> - T -> T) -> (list T))%ptype - then - _ <- ident.unify pattern.ident.List_update_nth List_update_nth; - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - x' <- base.try_make_transport_cps T b; - x'0 <- base.try_make_transport_cps T b; - v <- base.try_make_transport_cps T b; - x'1 <- base.try_make_transport_cps b b; - x'2 <- base.try_make_transport_cps b b; - v0 <- base.try_make_transport_cps b b; - v1 <- base.try_make_transport_cps b T; - v2 <- base.try_make_transport_cps T T; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) true - (#(nat_rect_arrow)%expr @ - (λ v3 : expr (list b), - (#(list_case)%expr @ - (λ _ : expr unit, - []%expr_pat) @ - (λ (v4 : expr b)(v5 : expr (list b)), - ($(x'2 (x'1 (x'0 (x' x0)))) @ $v4 :: $v5)%expr_pat) @ - $v3)%expr_pat)%expr @ - (λ (_ : expr ℕ)(v4 : expr (list b) -> - UnderLets (expr (list b))) - (v5 : expr (list b)), - (#(list_case)%expr @ - (λ _ : expr unit, - []%expr_pat) @ - (λ (v6 : expr b)(v7 : expr (list b)), - ($v6 :: $v4 @ $v7)%expr_pat) @ $v5)%expr_pat)%expr @ - (##(let (x2, _) := xv in x2))%expr @ - ($(v0 (v x1)))%expr)%expr_pat; - fv1 <-- do_again (list T) (v1 fv0); - Base (v2 fv1))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;;; - Base - (#(List_update_nth)%expr @ x @ (λ x2 : var T, - to_expr (x0 ($x2)))%expr @ x1)%expr_pat)%option -| @List_nth_default T => - fun (x : expr T) (x0 : expr (list T)) (x1 : expr ℕ) => - ((match x1 with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted - (((('1%pbtype -> (pattern.base.type.list '1) -> ℕ -> '1%pbtype) -> - '1%pbtype) -> (pattern.base.type.list '1)) -> ℕ)%ptype - ((((T -> (list T) -> ℕ -> T) -> T) -> (list T)) -> - (projT1 args))%ptype - with - | Datatypes.Some (_, (_, (_, _)), _, b0, _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((((b0 -> (list b0) -> ℕ -> b0) -> b0) -> (list b0)) -> ℕ)%ptype - ((((T -> (list T) -> ℕ -> T) -> T) -> (list T)) -> - (projT1 args))%ptype - then - _ <- ident.unify pattern.ident.List_nth_default - List_nth_default; - v <- base.try_make_transport_cps T b0; - v0 <- base.try_make_transport_cps T b0; - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - v1 <- base.try_make_transport_cps b0 b0; - v2 <- base.try_make_transport_cps b0 b0; - v3 <- base.try_make_transport_cps b0 T; - v4 <- base.try_make_transport_cps T T; - Datatypes.Some - (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement - (@Compile.reflect_ident_iota var) false - (#(eager_List_nth_default)%expr @ - ($(v1 (v x)))%expr @ ($(v2 (v0 x0)))%expr @ - (##(let (x2, _) := xv in x2))%expr)%expr_pat; - Base (v4 (v3 fv0)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(List_nth_default)%expr @ x @ x0 @ x1)%expr_pat)%option -| @eager_List_nth_default T => - fun (x : expr T) (x0 : expr (list T)) (x1 : expr ℕ) => - Base (#(eager_List_nth_default)%expr @ x @ x0 @ x1)%expr_pat -| Z_add => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) + - (let (x1, _) := xv0 in x1))%Z)%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (x + x0)%expr)%option -| Z_mul => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) * - (let (x1, _) := xv0 in x1))%Z)%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (x * x0)%expr)%option -| Z_pow => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) - ^ (let (x1, _) := xv0 in x1)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_pow)%expr @ x @ x0)%expr_pat)%option -| Z_sub => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) - - (let (x1, _) := xv0 in x1))%Z)%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (x - x0)%expr)%option -| Z_opp => - fun x : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match pattern.type.unify_extracted ℤ (projT1 args) with - | Datatypes.Some _ => - if type.type_beq base.type base.type.type_beq ℤ (projT1 args) - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some (Base (##(- (let (x0, _) := xv in x0))%Z)%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (- x)%expr)%option -| Z_div => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) / - (let (x1, _) := xv0 in x1))%Z)%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (x / x0)%expr)%option -| Z_modulo => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) - mod (let (x1, _) := xv0 in x1))%Z)%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (x mod x0)%expr)%option -| Z_log2 => - fun x : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match pattern.type.unify_extracted ℤ (projT1 args) with - | Datatypes.Some _ => - if type.type_beq base.type base.type.type_beq ℤ (projT1 args) - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base (##(Z.log2 (let (x0, _) := xv in x0)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_log2)%expr @ x)%expr_pat)%option -| Z_log2_up => - fun x : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match pattern.type.unify_extracted ℤ (projT1 args) with - | Datatypes.Some _ => - if type.type_beq base.type base.type.type_beq ℤ (projT1 args) - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base (##(Z.log2_up (let (x0, _) := xv in x0)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_log2_up)%expr @ x)%expr_pat)%option -| Z_eqb => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) =? - (let (x1, _) := xv0 in x1)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_eqb)%expr @ x @ x0)%expr_pat)%option -| Z_leb => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) <=? - (let (x1, _) := xv0 in x1)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_leb)%expr @ x @ x0)%expr_pat)%option -| Z_ltb => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) <? - (let (x1, _) := xv0 in x1)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_ltb)%expr @ x @ x0)%expr_pat)%option -| Z_geb => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) >=? - (let (x1, _) := xv0 in x1)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_geb)%expr @ x @ x0)%expr_pat)%option -| Z_gtb => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) >? - (let (x1, _) := xv0 in x1)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_gtb)%expr @ x @ x0)%expr_pat)%option -| Z_of_nat => - fun x : expr ℕ => - ((match x with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match pattern.type.unify_extracted ℕ (projT1 args) with - | Datatypes.Some _ => - if type.type_beq base.type base.type.type_beq ℕ (projT1 args) - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base (##(Z.of_nat (let (x0, _) := xv in x0)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_of_nat)%expr @ x)%expr_pat)%option -| Z_to_nat => - fun x : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match pattern.type.unify_extracted ℤ (projT1 args) with - | Datatypes.Some _ => - if type.type_beq base.type base.type.type_beq ℤ (projT1 args) - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base (##(Z.to_nat (let (x0, _) := xv in x0)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_to_nat)%expr @ x)%expr_pat)%option -| Z_shiftr => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) >> - (let (x1, _) := xv0 in x1))%Z)%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (x >> x0)%expr)%option -| Z_shiftl => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) << - (let (x1, _) := xv0 in x1))%Z)%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (x << x0)%expr)%option -| Z_land => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) &' - (let (x1, _) := xv0 in x1))%Z)%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (x &' x0)%expr)%option -| Z_lor => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##(Z.lor (let (x1, _) := xv in x1) - (let (x1, _) := xv0 in x1)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (x || x0)%expr)%option -| Z_min => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##(Z.min (let (x1, _) := xv in x1) - (let (x1, _) := xv0 in x1)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_min)%expr @ x @ x0)%expr_pat)%option -| Z_max => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##(Z.max (let (x1, _) := xv in x1) - (let (x1, _) := xv0 in x1)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_max)%expr @ x @ x0)%expr_pat)%option -| Z_bneg => - fun x : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - args <- invert_bind_args idc Raw.ident.Literal; - match pattern.type.unify_extracted ℤ (projT1 args) with - | Datatypes.Some _ => - if type.type_beq base.type base.type.type_beq ℤ (projT1 args) - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base (##(Z.bneg (let (x0, _) := xv in x0)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_bneg)%expr @ x)%expr_pat)%option -| Z_lnot_modulo => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##(Z.lnot_modulo (let (x1, _) := xv in x1) - (let (x1, _) := xv0 in x1)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_lnot_modulo)%expr @ x @ x0)%expr_pat)%option -| Z_mul_split => - fun x x0 x1 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - match x1 with - | @expr.Ident _ _ _ t1 idc1 => - args <- invert_bind_args idc1 Raw.ident.Literal; - args0 <- invert_bind_args idc0 Raw.ident.Literal; - args1 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal - ##(projT2 args1); - xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args0); - xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args); - Datatypes.Some - (Base - (let - '(a1, b1)%zrange := - Z.mul_split (let (x2, _) := xv in x2) - (let (x2, _) := xv0 in x2) - (let (x2, _) := xv1 in x2) in - ((##a1)%expr, (##b1)%expr)%expr_pat)) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat)%option -| Z_add_get_carry => - fun x x0 x1 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - match x1 with - | @expr.Ident _ _ _ t1 idc1 => - args <- invert_bind_args idc1 Raw.ident.Literal; - args0 <- invert_bind_args idc0 Raw.ident.Literal; - args1 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal - ##(projT2 args1); - xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args0); - xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args); - Datatypes.Some - (Base - (let - '(a1, b1)%zrange := - Z.add_get_carry_full (let (x2, _) := xv in x2) - (let (x2, _) := xv0 in x2) - (let (x2, _) := xv1 in x2) in - ((##a1)%expr, (##b1)%expr)%expr_pat)) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat)%option -| Z_add_with_carry => - fun x x0 x1 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - match x1 with - | @expr.Ident _ _ _ t1 idc1 => - args <- invert_bind_args idc1 Raw.ident.Literal; - args0 <- invert_bind_args idc0 Raw.ident.Literal; - args1 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal - ##(projT2 args1); - xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args0); - xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args); - Datatypes.Some - (Base - (##(Z.add_with_carry (let (x2, _) := xv in x2) - (let (x2, _) := xv0 in x2) - (let (x2, _) := xv1 in x2)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat)%option -| Z_add_with_get_carry => - fun x x0 x1 x2 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - match x1 with - | @expr.Ident _ _ _ t1 idc1 => - match x2 with - | @expr.Ident _ _ _ t2 idc2 => - args <- invert_bind_args idc2 Raw.ident.Literal; - args0 <- invert_bind_args idc1 Raw.ident.Literal; - args1 <- invert_bind_args idc0 Raw.ident.Literal; - args2 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - ((((projT1 args2) -> (projT1 args1)) -> - (projT1 args0)) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - ((((projT1 args2) -> (projT1 args1)) -> - (projT1 args0)) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal - ##(projT2 args2); - xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args1); - xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args0); - xv2 <- ident.unify pattern.ident.Literal - ##(projT2 args); - Datatypes.Some - (Base - (let - '(a2, b2)%zrange := - Z.add_with_get_carry_full - (let (x3, _) := xv in x3) - (let (x3, _) := xv0 in x3) - (let (x3, _) := xv1 in x3) - (let (x3, _) := xv2 in x3) in - ((##a2)%expr, (##b2)%expr)%expr_pat)) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat)%option -| Z_sub_get_borrow => - fun x x0 x1 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - match x1 with - | @expr.Ident _ _ _ t1 idc1 => - args <- invert_bind_args idc1 Raw.ident.Literal; - args0 <- invert_bind_args idc0 Raw.ident.Literal; - args1 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal - ##(projT2 args1); - xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args0); - xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args); - Datatypes.Some - (Base - (let - '(a1, b1)%zrange := - Z.sub_get_borrow_full (let (x2, _) := xv in x2) - (let (x2, _) := xv0 in x2) - (let (x2, _) := xv1 in x2) in - ((##a1)%expr, (##b1)%expr)%expr_pat)) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat)%option -| Z_sub_with_get_borrow => - fun x x0 x1 x2 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - match x1 with - | @expr.Ident _ _ _ t1 idc1 => - match x2 with - | @expr.Ident _ _ _ t2 idc2 => - args <- invert_bind_args idc2 Raw.ident.Literal; - args0 <- invert_bind_args idc1 Raw.ident.Literal; - args1 <- invert_bind_args idc0 Raw.ident.Literal; - args2 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - ((((projT1 args2) -> (projT1 args1)) -> - (projT1 args0)) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - ((((projT1 args2) -> (projT1 args1)) -> - (projT1 args0)) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal - ##(projT2 args2); - xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args1); - xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args0); - xv2 <- ident.unify pattern.ident.Literal - ##(projT2 args); - Datatypes.Some - (Base - (let - '(a2, b2)%zrange := - Z.sub_with_get_borrow_full - (let (x3, _) := xv in x3) - (let (x3, _) := xv0 in x3) - (let (x3, _) := xv1 in x3) - (let (x3, _) := xv2 in x3) in - ((##a2)%expr, (##b2)%expr)%expr_pat)) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_sub_with_get_borrow)%expr @ x @ x0 @ x1 @ x2)%expr_pat)%option -| Z_zselect => - fun x x0 x1 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - match x1 with - | @expr.Ident _ _ _ t1 idc1 => - args <- invert_bind_args idc1 Raw.ident.Literal; - args0 <- invert_bind_args idc0 Raw.ident.Literal; - args1 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal - ##(projT2 args1); - xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args0); - xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args); - Datatypes.Some - (Base - (##(Z.zselect (let (x2, _) := xv in x2) - (let (x2, _) := xv0 in x2) - (let (x2, _) := xv1 in x2)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_zselect)%expr @ x @ x0 @ x1)%expr_pat)%option -| Z_add_modulo => - fun x x0 x1 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - match x1 with - | @expr.Ident _ _ _ t1 idc1 => - args <- invert_bind_args idc1 Raw.ident.Literal; - args0 <- invert_bind_args idc0 Raw.ident.Literal; - args1 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal - ##(projT2 args1); - xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args0); - xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args); - Datatypes.Some - (Base - (##(Z.add_modulo (let (x2, _) := xv in x2) - (let (x2, _) := xv0 in x2) - (let (x2, _) := xv1 in x2)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_add_modulo)%expr @ x @ x0 @ x1)%expr_pat)%option -| Z_rshi => - fun x x0 x1 x2 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - match x1 with - | @expr.Ident _ _ _ t1 idc1 => - match x2 with - | @expr.Ident _ _ _ t2 idc2 => - args <- invert_bind_args idc2 Raw.ident.Literal; - args0 <- invert_bind_args idc1 Raw.ident.Literal; - args1 <- invert_bind_args idc0 Raw.ident.Literal; - args2 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - ((((projT1 args2) -> (projT1 args1)) -> - (projT1 args0)) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype - ((((projT1 args2) -> (projT1 args1)) -> - (projT1 args0)) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal - ##(projT2 args2); - xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args1); - xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args0); - xv2 <- ident.unify pattern.ident.Literal - ##(projT2 args); - Datatypes.Some - (Base - (##(Z.rshi (let (x3, _) := xv in x3) - (let (x3, _) := xv0 in x3) - (let (x3, _) := xv1 in x3) - (let (x3, _) := xv2 in x3)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat)%option -| Z_cc_m => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##(Z.cc_m (let (x1, _) := xv in x1) - (let (x1, _) := xv0 in x1)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_cc_m)%expr @ x @ x0)%expr_pat)%option -| Z_combine_at_bitwidth => - fun x x0 x1 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - match x1 with - | @expr.Ident _ _ _ t1 idc1 => - args <- invert_bind_args idc1 Raw.ident.Literal; - args0 <- invert_bind_args idc0 Raw.ident.Literal; - args1 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((ℤ -> ℤ) -> ℤ)%ptype - (((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal - ##(projT2 args1); - xv0 <- ident.unify pattern.ident.Literal - ##(projT2 args0); - xv1 <- ident.unify pattern.ident.Literal - ##(projT2 args); - Datatypes.Some - (Base - (##(Z.combine_at_bitwidth - (let (x2, _) := xv in x2) - (let (x2, _) := xv0 in x2) - (let (x2, _) := xv1 in x2)))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Z_combine_at_bitwidth)%expr @ x @ x0 @ x1)%expr_pat)%option -| Z_cast range => fun x : expr ℤ => Base (#(Z_cast range)%expr @ x)%expr_pat -| Z_cast2 range => - fun x : expr (ℤ * ℤ)%etype => Base (#(Z_cast2 range)%expr @ x)%expr_pat -| Some A => fun x : expr A => Base (#(Some)%expr @ x)%expr_pat -| None A => Base #(None)%expr -| @option_rect A P => - fun (x : expr A -> UnderLets (expr P)) - (x0 : expr unit -> UnderLets (expr P)) (x1 : expr (base.type.option A)) - => - Base - (#(option_rect)%expr @ (λ x2 : var A, - to_expr (x ($x2)))%expr @ - (λ x2 : var unit, - to_expr (x0 ($x2)))%expr @ x1)%expr_pat -| Build_zrange => - fun x x0 : expr ℤ => - ((match x with - | @expr.Ident _ _ _ t idc => - match x0 with - | @expr.Ident _ _ _ t0 idc0 => - args <- invert_bind_args idc0 Raw.ident.Literal; - args0 <- invert_bind_args idc Raw.ident.Literal; - match - pattern.type.unify_extracted (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - with - | Datatypes.Some (_, _)%zrange => - if - type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype - ((projT1 args0) -> (projT1 args))%ptype - then - xv <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##r[(let (x1, _) := xv in x1) ~> let (x1, _) := - xv0 in - x1]%zrange)%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | _ => Datatypes.None - end - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(Build_zrange)%expr @ x @ x0)%expr_pat)%option -| @zrange_rect P => - fun (x : expr ℤ -> expr ℤ -> UnderLets (expr P)) - (x0 : expr base.type.zrange) => - Base - (#(zrange_rect)%expr @ (λ x1 x2 : var ℤ, - to_expr (x ($x1) ($x2)))%expr @ x0)%expr_pat -| fancy_add log2wordmax imm => - fun x : expr (ℤ * ℤ)%etype => - Base (#(fancy_add log2wordmax imm)%expr @ x)%expr_pat -| fancy_addc log2wordmax imm => - fun x : expr (ℤ * ℤ * ℤ)%etype => - Base (#(fancy_addc log2wordmax imm)%expr @ x)%expr_pat -| fancy_sub log2wordmax imm => - fun x : expr (ℤ * ℤ)%etype => - Base (#(fancy_sub log2wordmax imm)%expr @ x)%expr_pat -| fancy_subb log2wordmax imm => - fun x : expr (ℤ * ℤ * ℤ)%etype => - Base (#(fancy_subb log2wordmax imm)%expr @ x)%expr_pat -| fancy_mulll log2wordmax => - fun x : expr (ℤ * ℤ)%etype => - Base (#(fancy_mulll log2wordmax)%expr @ x)%expr_pat -| fancy_mullh log2wordmax => - fun x : expr (ℤ * ℤ)%etype => - Base (#(fancy_mullh log2wordmax)%expr @ x)%expr_pat -| fancy_mulhl log2wordmax => - fun x : expr (ℤ * ℤ)%etype => - Base (#(fancy_mulhl log2wordmax)%expr @ x)%expr_pat -| fancy_mulhh log2wordmax => - fun x : expr (ℤ * ℤ)%etype => - Base (#(fancy_mulhh log2wordmax)%expr @ x)%expr_pat -| fancy_rshi log2wordmax x => - fun x0 : expr (ℤ * ℤ)%etype => - Base (#(fancy_rshi log2wordmax x)%expr @ x0)%expr_pat -| fancy_selc => - fun x : expr (ℤ * ℤ * ℤ)%etype => - ((match x with - | (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident - _ _ _ t2 idc2) @ @expr.Ident _ _ _ t3 idc3)%expr_pat => - args <- invert_bind_args idc3 Raw.ident.Literal; - args0 <- invert_bind_args idc2 Raw.ident.Literal; - args1 <- invert_bind_args idc1 Raw.ident.Literal; - args2 <- invert_bind_args idc0 Raw.ident.pair; - args3 <- invert_bind_args idc Raw.ident.pair; - match - pattern.type.unify_extracted - ((((ℤ * ℤ)%pbtype -> ℤ -> (ℤ * ℤ * ℤ)%pbtype) -> - ((ℤ -> ℤ -> (ℤ * ℤ)%pbtype) -> ℤ) -> ℤ) -> ℤ)%ptype - ((((let (x4, _) := args3 in x4) -> - (let (_, y) := args3 in y) -> - ((let (x4, _) := args3 in x4) * (let (_, y) := args3 in y))%etype) -> - (((let (x4, _) := args2 in x4) -> - (let (_, y) := args2 in y) -> - ((let (x4, _) := args2 in x4) * (let (_, y) := args2 in y))%etype) -> - (projT1 args1)) -> (projT1 args0)) -> (projT1 args))%ptype - with - | Datatypes.Some - (_, _, (_, (_, _, _)), (_, (_, (_, _)), _, _), _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((((ℤ * ℤ)%etype -> ℤ -> (ℤ * ℤ * ℤ)%etype) -> - ((ℤ -> ℤ -> (ℤ * ℤ)%etype) -> ℤ) -> ℤ) -> ℤ)%ptype - ((((let (x4, _) := args3 in x4) -> - (let (_, y) := args3 in y) -> - ((let (x4, _) := args3 in x4) * - (let (_, y) := args3 in y))%etype) -> - (((let (x4, _) := args2 in x4) -> - (let (_, y) := args2 in y) -> - ((let (x4, _) := args2 in x4) * - (let (_, y) := args2 in y))%etype) -> (projT1 args1)) -> - (projT1 args0)) -> (projT1 args))%ptype - then - _ <- ident.unify pattern.ident.pair pair; - _ <- ident.unify pattern.ident.pair pair; - xv <- ident.unify pattern.ident.Literal ##(projT2 args1); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##(fancy.interp - (Option.invert_Some (to_fancy fancy_selc)) - (let (x4, _) := xv in x4, let (x4, _) := xv0 in x4, - let (x4, _) := xv1 in x4)%zrange))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident - _ _ _ t2 idc2) @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident - _ _ _ t2 idc2) @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident - _ _ _ t2 idc2) @ (_ @ _))%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident - _ _ _ t2 idc2) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => - Datatypes.None - | (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ ($_)%expr) @ - _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ - _ _ _ _ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ (_ @ _)) @ - _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.LetIn - _ _ _ _ _ _ _) @ _)%expr_pat => Datatypes.None - | (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ ($_)%expr @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ (_ @ _) @ _) @ - _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat => - Datatypes.None - | (@expr.Ident _ _ _ t idc @ #(_) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ ($_)%expr @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (#(_) @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (($_)%expr @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (($_)%expr @ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (@expr.Abs _ _ _ _ _ _ @ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (_ @ _ @ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => - Datatypes.None - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(fancy_selc)%expr @ x)%expr_pat)%option -| fancy_selm log2wordmax => - fun x : expr (ℤ * ℤ * ℤ)%etype => - Base (#(fancy_selm log2wordmax)%expr @ x)%expr_pat -| fancy_sell => - fun x : expr (ℤ * ℤ * ℤ)%etype => - ((match x with - | (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident - _ _ _ t2 idc2) @ @expr.Ident _ _ _ t3 idc3)%expr_pat => - args <- invert_bind_args idc3 Raw.ident.Literal; - args0 <- invert_bind_args idc2 Raw.ident.Literal; - args1 <- invert_bind_args idc1 Raw.ident.Literal; - args2 <- invert_bind_args idc0 Raw.ident.pair; - args3 <- invert_bind_args idc Raw.ident.pair; - match - pattern.type.unify_extracted - ((((ℤ * ℤ)%pbtype -> ℤ -> (ℤ * ℤ * ℤ)%pbtype) -> - ((ℤ -> ℤ -> (ℤ * ℤ)%pbtype) -> ℤ) -> ℤ) -> ℤ)%ptype - ((((let (x4, _) := args3 in x4) -> - (let (_, y) := args3 in y) -> - ((let (x4, _) := args3 in x4) * (let (_, y) := args3 in y))%etype) -> - (((let (x4, _) := args2 in x4) -> - (let (_, y) := args2 in y) -> - ((let (x4, _) := args2 in x4) * (let (_, y) := args2 in y))%etype) -> - (projT1 args1)) -> (projT1 args0)) -> (projT1 args))%ptype - with - | Datatypes.Some - (_, _, (_, (_, _, _)), (_, (_, (_, _)), _, _), _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((((ℤ * ℤ)%etype -> ℤ -> (ℤ * ℤ * ℤ)%etype) -> - ((ℤ -> ℤ -> (ℤ * ℤ)%etype) -> ℤ) -> ℤ) -> ℤ)%ptype - ((((let (x4, _) := args3 in x4) -> - (let (_, y) := args3 in y) -> - ((let (x4, _) := args3 in x4) * - (let (_, y) := args3 in y))%etype) -> - (((let (x4, _) := args2 in x4) -> - (let (_, y) := args2 in y) -> - ((let (x4, _) := args2 in x4) * - (let (_, y) := args2 in y))%etype) -> (projT1 args1)) -> - (projT1 args0)) -> (projT1 args))%ptype - then - _ <- ident.unify pattern.ident.pair pair; - _ <- ident.unify pattern.ident.pair pair; - xv <- ident.unify pattern.ident.Literal ##(projT2 args1); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##(fancy.interp - (Option.invert_Some (to_fancy fancy_sell)) - (let (x4, _) := xv in x4, let (x4, _) := xv0 in x4, - let (x4, _) := xv1 in x4)%zrange))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident - _ _ _ t2 idc2) @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident - _ _ _ t2 idc2) @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident - _ _ _ t2 idc2) @ (_ @ _))%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident - _ _ _ t2 idc2) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => - Datatypes.None - | (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ ($_)%expr) @ - _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ - _ _ _ _ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ (_ @ _)) @ - _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.LetIn - _ _ _ _ _ _ _) @ _)%expr_pat => Datatypes.None - | (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ ($_)%expr @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ (_ @ _) @ _) @ - _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat => - Datatypes.None - | (@expr.Ident _ _ _ t idc @ #(_) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ ($_)%expr @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (#(_) @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (($_)%expr @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (($_)%expr @ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (@expr.Abs _ _ _ _ _ _ @ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (_ @ _ @ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => - Datatypes.None - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(fancy_sell)%expr @ x)%expr_pat)%option -| fancy_addm => - fun x : expr (ℤ * ℤ * ℤ)%etype => - ((match x with - | (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident - _ _ _ t2 idc2) @ @expr.Ident _ _ _ t3 idc3)%expr_pat => - args <- invert_bind_args idc3 Raw.ident.Literal; - args0 <- invert_bind_args idc2 Raw.ident.Literal; - args1 <- invert_bind_args idc1 Raw.ident.Literal; - args2 <- invert_bind_args idc0 Raw.ident.pair; - args3 <- invert_bind_args idc Raw.ident.pair; - match - pattern.type.unify_extracted - ((((ℤ * ℤ)%pbtype -> ℤ -> (ℤ * ℤ * ℤ)%pbtype) -> - ((ℤ -> ℤ -> (ℤ * ℤ)%pbtype) -> ℤ) -> ℤ) -> ℤ)%ptype - ((((let (x4, _) := args3 in x4) -> - (let (_, y) := args3 in y) -> - ((let (x4, _) := args3 in x4) * (let (_, y) := args3 in y))%etype) -> - (((let (x4, _) := args2 in x4) -> - (let (_, y) := args2 in y) -> - ((let (x4, _) := args2 in x4) * (let (_, y) := args2 in y))%etype) -> - (projT1 args1)) -> (projT1 args0)) -> (projT1 args))%ptype - with - | Datatypes.Some - (_, _, (_, (_, _, _)), (_, (_, (_, _)), _, _), _)%zrange => - if - type.type_beq base.type base.type.type_beq - ((((ℤ * ℤ)%etype -> ℤ -> (ℤ * ℤ * ℤ)%etype) -> - ((ℤ -> ℤ -> (ℤ * ℤ)%etype) -> ℤ) -> ℤ) -> ℤ)%ptype - ((((let (x4, _) := args3 in x4) -> - (let (_, y) := args3 in y) -> - ((let (x4, _) := args3 in x4) * - (let (_, y) := args3 in y))%etype) -> - (((let (x4, _) := args2 in x4) -> - (let (_, y) := args2 in y) -> - ((let (x4, _) := args2 in x4) * - (let (_, y) := args2 in y))%etype) -> (projT1 args1)) -> - (projT1 args0)) -> (projT1 args))%ptype - then - _ <- ident.unify pattern.ident.pair pair; - _ <- ident.unify pattern.ident.pair pair; - xv <- ident.unify pattern.ident.Literal ##(projT2 args1); - xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); - xv1 <- ident.unify pattern.ident.Literal ##(projT2 args); - Datatypes.Some - (Base - (##(fancy.interp - (Option.invert_Some (to_fancy fancy_addm)) - (let (x4, _) := xv in x4, let (x4, _) := xv0 in x4, - let (x4, _) := xv1 in x4)%zrange))%expr) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident - _ _ _ t2 idc2) @ ($_)%expr)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident - _ _ _ t2 idc2) @ @expr.Abs _ _ _ _ _ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident - _ _ _ t2 idc2) @ (_ @ _))%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Ident - _ _ _ t2 idc2) @ @expr.LetIn _ _ _ _ _ _ _)%expr_pat => - Datatypes.None - | (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ ($_)%expr) @ - _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.Abs _ - _ _ _ _ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ (_ @ _)) @ - _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Ident _ _ _ t1 idc1 @ @expr.LetIn - _ _ _ _ _ _ _) @ _)%expr_pat => Datatypes.None - | (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ ($_)%expr @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (@expr.Ident _ _ _ t0 idc0 @ (_ @ _) @ _) @ - _)%expr_pat | - (@expr.Ident _ _ _ t idc @ - (@expr.Ident _ _ _ t0 idc0 @ @expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat => - Datatypes.None - | (@expr.Ident _ _ _ t idc @ #(_) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ ($_)%expr @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ @expr.Abs _ _ _ _ _ _ @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (#(_) @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (($_)%expr @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (@expr.Abs _ _ _ _ _ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (($_)%expr @ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (@expr.Abs _ _ _ _ _ _ @ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (_ @ _ @ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (@expr.LetIn _ _ _ _ _ _ _ @ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ (@expr.LetIn _ _ _ _ _ _ _ @ _) @ _)%expr_pat | - (@expr.Ident _ _ _ t idc @ @expr.LetIn _ _ _ _ _ _ _ @ _)%expr_pat => - Datatypes.None - | _ => Datatypes.None - end;; - Datatypes.None);;; - Base (#(fancy_addm)%expr @ x)%expr_pat)%option -end - : Compile.value' true t |