aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-11-01 17:55:49 -0400
committerGravatar Jason Gross <jgross@mit.edu>2018-11-01 17:55:49 -0400
commit42147086fe3049b6622d95e3c71792d80bf43ae3 (patch)
tree886e7a2fb7c70afd64cb562f6a70ebb02ad17d8e /src
parentf02258707a08518df4ad9df0b100aea684f4df31 (diff)
Also inline Z_cast things
Diffstat (limited to 'src')
-rw-r--r--src/Experiments/NewPipeline/README.md2
-rw-r--r--src/Experiments/NewPipeline/Rewriter.v4
-rw-r--r--src/Experiments/NewPipeline/RewriterRulesGood.v2
-rw-r--r--src/Experiments/NewPipeline/UnderLets.v12
-rw-r--r--src/Experiments/NewPipeline/UnderLetsProofs.v18
-rw-r--r--src/Experiments/NewPipeline/arith_rewrite_head.out168
-rw-r--r--src/Experiments/NewPipeline/fancy_rewrite_head.out86
-rw-r--r--src/Experiments/NewPipeline/nbe_rewrite_head.out128
8 files changed, 212 insertions, 208 deletions
diff --git a/src/Experiments/NewPipeline/README.md b/src/Experiments/NewPipeline/README.md
index e1b3b5b16..72c5f3a89 100644
--- a/src/Experiments/NewPipeline/README.md
+++ b/src/Experiments/NewPipeline/README.md
@@ -45,7 +45,7 @@ The files contain:
substituting away var-like things (this is used to ensure that when we output
C code, aliasing the input and the output arrays doesn't cause issues).
Defines the passes:
- + SubstVarFstSndPairOpp
+ + SubstVarFstSndPairOppCast
- AbstractInterpretation.v: type-code-based ZRange definitions, abstract
interpretation of identifiers (which does let-lifting, for historical reasons,
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index 8c532f19c..b8c8bdead 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -1904,7 +1904,7 @@ Module Compilers.
; make_rewrite_step (* _step, so that if one of the arguments is concrete, we automatically get the rewrite rule for [Z_cast] applying to it *)
(#pattern.ident.Z_cast2 @ (??, ??)) (fun r x y => (#(ident.Z_cast (fst r)) @ $x, #(ident.Z_cast (snd r)) @ $y))
- ; make_rewriteol (-??) (fun e => (llet v := e in -$v) when negb (SubstVarLike.is_var_fst_snd_pair_opp e)) (* inline negation when the rewriter wouldn't already inline it *)
+ ; make_rewriteol (-??) (fun e => (llet v := e in -$v) when negb (SubstVarLike.is_var_fst_snd_pair_opp_cast e)) (* inline negation when the rewriter wouldn't already inline it *)
].
Definition arith_with_casts_rewrite_rules : rewrite_rulesT
@@ -2200,7 +2200,7 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y)
Compile.option_bind' pident_unify_unknown invert_bind_args_unknown Compile.normalize_deep_rewrite_rule
Compile.reflect UnderLets.reify_and_let_binds_base_cps Compile.reify Compile.reify_and_let_binds_cps
Compile.value'
- SubstVarLike.is_var_fst_snd_pair_opp
+ SubstVarLike.is_var_fst_snd_pair_opp_cast
] in rewrite_head0).
Ltac timed_make_rewrite_head1 rewrite_head0 pr2_rewrite_rules :=
constr:(ltac:(time (idtac; let v := make_rewrite_head1 rewrite_head0 pr2_rewrite_rules in exact v))).
diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v
index ef29c9c0b..d66e02998 100644
--- a/src/Experiments/NewPipeline/RewriterRulesGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesGood.v
@@ -235,7 +235,7 @@ Module Compilers.
| progress cbn [pattern.ident.arg_types] in *
| progress cbn [fst snd projT1 projT2] in *
| progress intros
- | progress cbv [id pattern.ident.arg_types Compile.value cpsbind cpscall cpsreturn cps_option_bind type_base ident.smart_Literal rwhen rwhenl nth_default SubstVarLike.is_var_fst_snd_pair_opp] in *
+ | progress cbv [id pattern.ident.arg_types Compile.value cpsbind cpscall cpsreturn cps_option_bind type_base ident.smart_Literal rwhen rwhenl nth_default SubstVarLike.is_var_fst_snd_pair_opp_cast] in *
| progress cbv [Compile.option_bind'] in *
| progress type_beq_to_eq
| progress type.inversion_type
diff --git a/src/Experiments/NewPipeline/UnderLets.v b/src/Experiments/NewPipeline/UnderLets.v
index 689d53ee1..dd6019570 100644
--- a/src/Experiments/NewPipeline/UnderLets.v
+++ b/src/Experiments/NewPipeline/UnderLets.v
@@ -69,15 +69,17 @@ Module Compilers.
| ident.fst _ _
| ident.snd _ _
| ident.Z_opp
+ | ident.Z_cast _
+ | ident.Z_cast2 _
=> true
| _ => false
end.
- Definition is_var_fst_snd_pair_opp {var} {t} (e : expr (var:=var) t) : bool
+ Definition is_var_fst_snd_pair_opp_cast {var} {t} (e : expr (var:=var) t) : bool
:= @is_recursively_var_or_ident base.type ident var (@ident_is_var_like) t e.
- Definition IsVarFstSndPairOpp {t} (e : expr.Expr t) : bool
- := @is_var_fst_snd_pair_opp (fun _ => unit) t (e _).
+ Definition IsVarFstSndPairOppCast {t} (e : expr.Expr t) : bool
+ := @is_var_fst_snd_pair_opp_cast (fun _ => unit) t (e _).
- Definition SubstVarFstSndPairOpp {t} (e : expr.Expr t) : expr.Expr t
+ Definition SubstVarFstSndPairOppCast {t} (e : expr.Expr t) : expr.Expr t
:= @SubstVarOrIdent base.type ident (@ident_is_var_like) t e.
End SubstVarLike.
@@ -139,7 +141,7 @@ Module Compilers.
:= fun e T k
=> match invert_expr.invert_Var e with
| Some v => k ($v)%expr
- | None => if SubstVarLike.is_var_fst_snd_pair_opp e
+ | None => if SubstVarLike.is_var_fst_snd_pair_opp_cast e
then k e
else UnderLets.UnderLet e (fun v => k ($v)%expr)
end.
diff --git a/src/Experiments/NewPipeline/UnderLetsProofs.v b/src/Experiments/NewPipeline/UnderLetsProofs.v
index dcc5cf28b..837aba4b4 100644
--- a/src/Experiments/NewPipeline/UnderLetsProofs.v
+++ b/src/Experiments/NewPipeline/UnderLetsProofs.v
@@ -140,8 +140,8 @@ Module Compilers.
End interp.
End with_ident.
- Lemma Wf_SubstVarFstSndPairOpp {t} (e : expr.Expr t)
- : expr.Wf e -> expr.Wf (SubstVarLike.SubstVarFstSndPairOpp e).
+ Lemma Wf_SubstVarFstSndPairOppCast {t} (e : expr.Expr t)
+ : expr.Wf e -> expr.Wf (SubstVarLike.SubstVarFstSndPairOppCast e).
Proof. apply Wf_SubstVarOrIdent. Qed.
Section with_cast.
@@ -150,14 +150,14 @@ Module Compilers.
Local Notation interp := (@expr.interp _ _ _ (@ident_interp)).
Local Notation Interp := (@expr.Interp _ _ _ (@ident_interp)).
- Lemma Interp_SubstVarFstSndPairOpp {t} (e : expr.Expr t) (Hwf : expr.Wf e)
- : Interp (SubstVarLike.SubstVarFstSndPairOpp e) == Interp e.
+ Lemma Interp_SubstVarFstSndPairOppCast {t} (e : expr.Expr t) (Hwf : expr.Wf e)
+ : Interp (SubstVarLike.SubstVarFstSndPairOppCast e) == Interp e.
Proof. apply Interp_SubstVarOrIdent, Hwf. Qed.
End with_cast.
End SubstVarLike.
- Hint Resolve SubstVarLike.Wf_SubstVar SubstVarLike.Wf_SubstVarFstSndPairOpp SubstVarLike.Wf_SubstVarLike SubstVarLike.Wf_SubstVarOrIdent : wf.
- Hint Rewrite @SubstVarLike.Interp_SubstVar @SubstVarLike.Interp_SubstVarFstSndPairOpp @SubstVarLike.Interp_SubstVarLike @SubstVarLike.Interp_SubstVarOrIdent : interp.
+ Hint Resolve SubstVarLike.Wf_SubstVar SubstVarLike.Wf_SubstVarFstSndPairOppCast SubstVarLike.Wf_SubstVarLike SubstVarLike.Wf_SubstVarOrIdent : wf.
+ Hint Rewrite @SubstVarLike.Interp_SubstVar @SubstVarLike.Interp_SubstVarFstSndPairOppCast @SubstVarLike.Interp_SubstVarLike @SubstVarLike.Interp_SubstVarOrIdent : interp.
Module UnderLets.
Import UnderLets.Compilers.UnderLets.
@@ -426,7 +426,7 @@ Module Compilers.
: wf P G (reify_and_let_binds_base_cps e1 T1 k1) (reify_and_let_binds_base_cps e2 T2 k2).
Proof.
revert dependent G; induction t; cbn [reify_and_let_binds_base_cps]; intros;
- try (cbv [SubstVarLike.is_var_fst_snd_pair_opp] in *; erewrite !SubstVarLike.wfT_is_recursively_var_or_ident by eassumption);
+ try (cbv [SubstVarLike.is_var_fst_snd_pair_opp_cast] in *; erewrite !SubstVarLike.wfT_is_recursively_var_or_ident by eassumption);
break_innermost_match; wf_reify_and_let_binds_base_cps_t Hk.
all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end.
all: revert dependent k1; revert dependent k2.
@@ -502,7 +502,7 @@ Module Compilers.
| apply (f_equal2 (@cons _))
| match goal with
| [ H : _ |- _ ] => apply H; clear H
- | [ H : SubstVarLike.is_var_fst_snd_pair_opp (reify_list _) = _ |- _ ] => clear H
+ | [ H : SubstVarLike.is_var_fst_snd_pair_opp_cast (reify_list _) = _ |- _ ] => clear H
| [ H : context[interp (reify_list _)] |- _ ]
=> rewrite expr.interp_reify_list in H
| [ |- ?Q (UnderLets.interp _ (list_rect ?P ?X ?Y ?ls ?k)) ]
@@ -597,7 +597,7 @@ Module Compilers.
: interp (to_expr (reify_and_let_binds_base_cps e1 _ k1)) == k2 (interp e2).
Proof.
revert dependent G; revert dependent t'; induction t; cbn [reify_and_let_binds_base_cps]; intros;
- try (cbv [SubstVarLike.is_var_fst_snd_pair_opp] in *; erewrite !SubstVarLike.wfT_is_recursively_var_or_ident by eassumption);
+ try (cbv [SubstVarLike.is_var_fst_snd_pair_opp_cast] in *; erewrite !SubstVarLike.wfT_is_recursively_var_or_ident by eassumption);
break_innermost_match; interp_to_expr_reify_and_let_binds_base_cps_t Hk.
all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end.
all: revert dependent k1; revert dependent k2.
diff --git a/src/Experiments/NewPipeline/arith_rewrite_head.out b/src/Experiments/NewPipeline/arith_rewrite_head.out
index 112dd2250..43d55747c 100644
--- a/src/Experiments/NewPipeline/arith_rewrite_head.out
+++ b/src/Experiments/NewPipeline/arith_rewrite_head.out
@@ -27,7 +27,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) ->
s0) -> s)%ptype option (fun x2 : option => x2)
with
- | Some (_, _, _, (_, (_, (_, _)), b3, b2)) =>
+ | Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange =>
if
type.type_beq base.type base.type.type_beq
(((b3 * b2)%etype -> b3) ->
@@ -78,7 +78,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) ->
s0) -> s)%ptype option (fun x2 : option => x2)
with
- | Some (_, _, _, (_, (_, (_, _)), b3, b2)) =>
+ | Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange =>
if
type.type_beq base.type base.type.type_beq
(((b3 * b2)%etype -> b2) ->
@@ -222,7 +222,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype
@@ -244,7 +244,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype
@@ -267,7 +267,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(s -> (projT1 args0))%ptype option
(fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(ℤ -> ℤ)%ptype (s -> (projT1 args0))%ptype
@@ -291,7 +291,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(s -> (projT1 args0))%ptype option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(s -> (projT1 args0))%ptype
@@ -324,7 +324,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args) -> s)%ptype option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(ℤ -> ℤ)%ptype ((projT1 args) -> s)%ptype
@@ -348,7 +348,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args) -> s)%ptype option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args) -> s)%ptype
@@ -374,7 +374,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(s0 -> s)%ptype option (fun x3 : option => x3)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(s0 -> s)%ptype
@@ -406,7 +406,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s -> ℤ)%ptype
option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(s -> ℤ)%ptype
@@ -428,7 +428,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> s)%ptype
option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> s)%ptype
@@ -458,7 +458,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -481,7 +481,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype
@@ -503,7 +503,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype
@@ -525,7 +525,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype
@@ -547,7 +547,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype
@@ -569,7 +569,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(s -> (projT1 args0))%ptype option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(s -> (projT1 args0))%ptype
@@ -598,7 +598,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args) -> s)%ptype option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args) -> s)%ptype
@@ -627,7 +627,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype
@@ -649,7 +649,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype
@@ -671,7 +671,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype
@@ -695,7 +695,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype
@@ -719,7 +719,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(s0 -> s)%ptype option (fun x3 : option => x3)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(s0 -> s)%ptype
@@ -750,7 +750,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s -> ℤ)%ptype
option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(s -> ℤ)%ptype
@@ -772,7 +772,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype
@@ -796,7 +796,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> s)%ptype
option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> s)%ptype
@@ -818,7 +818,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype
@@ -856,7 +856,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args2) -> (projT1 args0) -> s2 -> s1)%ptype
option (fun x5 : option => x5)
with
- | Some (_, (_, (_, _))) =>
+ | Some (_, (_, (_, _)))%zrange =>
if
type.type_beq base.type base.type.type_beq
(ℤ -> ℤ -> ℤ -> ℤ)%ptype
@@ -913,7 +913,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args2) -> s0 -> s2 -> (projT1 args))%ptype
option (fun x5 : option => x5)
with
- | Some (_, (_, (_, _))) =>
+ | Some (_, (_, (_, _)))%zrange =>
if
type.type_beq base.type base.type.type_beq
(ℤ -> ℤ -> ℤ -> ℤ)%ptype
@@ -963,7 +963,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> s0 -> s)%ptype option
(fun x3 : option => x3)
with
- | Some (_, (_, _)) =>
+ | Some (_, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
(ℤ -> ℤ -> ℤ)%ptype ((projT1 args0) -> s0 -> s)%ptype
@@ -1001,7 +1001,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype
@@ -1034,7 +1034,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args0) -> s)%ptype option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> s)%ptype
@@ -1059,7 +1059,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype
@@ -1081,7 +1081,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype
@@ -1103,7 +1103,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args) -> s)%ptype option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(ℤ -> ℤ)%ptype ((projT1 args) -> s)%ptype
@@ -1127,7 +1127,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args) -> s)%ptype option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args) -> s)%ptype
@@ -1159,7 +1159,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype
@@ -1183,7 +1183,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(s -> (projT1 args))%ptype option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(ℤ -> ℤ)%ptype (s -> (projT1 args))%ptype
@@ -1208,7 +1208,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(s -> (projT1 args))%ptype option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(s -> (projT1 args))%ptype
@@ -1240,7 +1240,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype
@@ -1264,7 +1264,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(s0 -> s)%ptype option (fun x3 : option => x3)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(s0 -> s)%ptype
@@ -1295,7 +1295,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (s -> ℤ)%ptype
option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(s -> ℤ)%ptype
@@ -1317,7 +1317,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype (ℤ -> s)%ptype
option (fun x2 : option => x2)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> s)%ptype
@@ -1362,7 +1362,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
| Some _ =>
if type.type_beq base.type base.type.type_beq ℤ ℤ
then
- fv <- (if negb (SubstVarLike.is_var_fst_snd_pair_opp x)
+ fv <- (if negb (SubstVarLike.is_var_fst_snd_pair_opp_cast x)
then
Some
(UnderLet x
@@ -1388,7 +1388,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype
@@ -1406,7 +1406,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype
@@ -1436,7 +1436,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype
@@ -1454,7 +1454,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype
@@ -1492,7 +1492,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
(ℤ -> (projT1 args))%ptype
@@ -1514,7 +1514,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype option (fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args) -> ℤ)%ptype
@@ -1548,7 +1548,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args0) -> (projT1 args)) -> ℤ)%ptype option
(fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -1575,7 +1575,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args0) -> ℤ) -> (projT1 args))%ptype option
(fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -1602,7 +1602,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args0) -> (projT1 args)) -> ℤ)%ptype option
(fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -1629,7 +1629,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args0) -> ℤ) -> (projT1 args))%ptype option
(fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -1656,7 +1656,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args0) -> (projT1 args)) -> ℤ)%ptype option
(fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -1683,7 +1683,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args0) -> ℤ) -> (projT1 args))%ptype option
(fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -1707,7 +1707,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
((ℤ -> ℤ) -> ℤ)%ptype option (fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq ((ℤ -> ℤ) -> ℤ)%ptype
((ℤ -> ℤ) -> ℤ)%ptype
@@ -1731,7 +1731,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
((ℤ -> s) -> ℤ)%ptype option (fun x3 : option => x3)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> s) -> ℤ)%ptype
@@ -1760,7 +1760,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
((ℤ -> ℤ) -> s)%ptype option (fun x3 : option => x3)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> ℤ) -> s)%ptype
@@ -1790,7 +1790,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((ℤ -> (projT1 args)) -> ℤ)%ptype option
(fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> (projT1 args)) -> ℤ)%ptype
@@ -1822,7 +1822,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((ℤ -> ℤ) -> (projT1 args))%ptype option
(fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> ℤ) -> (projT1 args))%ptype
@@ -1854,7 +1854,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((ℤ -> (projT1 args)) -> ℤ)%ptype option
(fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> (projT1 args)) -> ℤ)%ptype
@@ -1877,7 +1877,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((ℤ -> ℤ) -> (projT1 args))%ptype option
(fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> ℤ) -> (projT1 args))%ptype
@@ -1896,7 +1896,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
((ℤ -> ℤ) -> ℤ)%ptype option (fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq ((ℤ -> ℤ) -> ℤ)%ptype
((ℤ -> ℤ) -> ℤ)%ptype
@@ -1921,7 +1921,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args) -> ℤ) -> ℤ)%ptype option
(fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype (((projT1 args) -> ℤ) -> ℤ)%ptype
@@ -1940,7 +1940,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
((ℤ -> ℤ) -> ℤ)%ptype option (fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq ((ℤ -> ℤ) -> ℤ)%ptype
((ℤ -> ℤ) -> ℤ)%ptype
@@ -1967,7 +1967,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((ℤ -> (projT1 args0)) -> s) -> ℤ)%ptype option
(fun x4 : option => x4)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2000,7 +2000,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((ℤ -> (projT1 args0)) -> s) -> ℤ)%ptype option
(fun x4 : option => x4)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2041,7 +2041,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((ℤ -> (projT1 args0)) -> ℤ) -> s)%ptype option
(fun x4 : option => x4)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2074,7 +2074,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((ℤ -> (projT1 args0)) -> ℤ) -> s)%ptype option
(fun x4 : option => x4)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2115,7 +2115,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((ℤ -> (projT1 args0)) -> (projT1 args)) -> ℤ)%ptype
option (fun x3 : option => x3)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2159,7 +2159,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((ℤ -> (projT1 args0)) -> ℤ) -> (projT1 args))%ptype
option (fun x3 : option => x3)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2206,7 +2206,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((projT1 args0) -> (projT1 args1)) -> (projT1 args)) ->
ℤ)%ptype option (fun x3 : option => x3)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2241,7 +2241,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((projT1 args0) -> (projT1 args1)) -> ℤ) ->
(projT1 args))%ptype option (fun x3 : option => x3)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2273,7 +2273,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((ℤ -> (projT1 args)) -> ℤ) -> ℤ)%ptype option
(fun x3 : option => x3)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2305,7 +2305,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype (((ℤ -> s) -> s0) -> ℤ)%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2340,7 +2340,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype (((ℤ -> s) -> ℤ) -> s0)%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2376,7 +2376,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((ℤ -> s) -> (projT1 args)) -> ℤ)%ptype option
(fun x4 : option => x4)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2414,7 +2414,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((ℤ -> s) -> ℤ) -> (projT1 args))%ptype option
(fun x4 : option => x4)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2459,7 +2459,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((ℤ -> ℤ) -> (projT1 args0)) -> (projT1 args))%ptype
option (fun x3 : option => x3)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2495,7 +2495,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype option (fun x3 : option => x3)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2517,7 +2517,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
((ℤ -> ℤ) -> ℤ)%ptype option (fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq ((ℤ -> ℤ) -> ℤ)%ptype
((ℤ -> ℤ) -> ℤ)%ptype
@@ -2537,7 +2537,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype option (fun x3 : option => x3)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2576,7 +2576,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) ->
s0) -> s)%ptype option (fun x2 : option => x2)
with
- | Some (_, (_, (_, _)), _, _) =>
+ | Some (_, (_, (_, _)), _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ -> (ℤ * ℤ)%etype) -> ℤ) -> ℤ)%ptype
diff --git a/src/Experiments/NewPipeline/fancy_rewrite_head.out b/src/Experiments/NewPipeline/fancy_rewrite_head.out
index d6ae37896..afe8cab0f 100644
--- a/src/Experiments/NewPipeline/fancy_rewrite_head.out
+++ b/src/Experiments/NewPipeline/fancy_rewrite_head.out
@@ -131,7 +131,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args1) -> s0 -> (projT1 args))%ptype option
(fun x3 : option => x3)
with
- | Some (_, (_, _)) =>
+ | Some (_, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
(ℤ -> ℤ -> ℤ)%ptype
@@ -177,7 +177,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args1) -> (projT1 args) -> s)%ptype option
(fun x3 : option => x3)
with
- | Some (_, (_, _)) =>
+ | Some (_, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
(ℤ -> ℤ -> ℤ)%ptype
@@ -219,7 +219,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args1) -> (projT1 args) -> s)%ptype option
(fun x3 : option => x3)
with
- | Some (_, (_, _)) =>
+ | Some (_, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
(ℤ -> ℤ -> ℤ)%ptype
@@ -265,7 +265,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args1) -> s0 -> (projT1 args))%ptype option
(fun x3 : option => x3)
with
- | Some (_, (_, _)) =>
+ | Some (_, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
(ℤ -> ℤ -> ℤ)%ptype
@@ -311,7 +311,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args1) -> s0 -> (projT1 args))%ptype option
(fun x3 : option => x3)
with
- | Some (_, (_, _)) =>
+ | Some (_, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
(ℤ -> ℤ -> ℤ)%ptype
@@ -341,7 +341,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args1) -> s0 -> (projT1 args))%ptype option
(fun x3 : option => x3)
with
- | Some (_, (_, _)) =>
+ | Some (_, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
(ℤ -> ℤ -> ℤ)%ptype
@@ -390,7 +390,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args0) -> s) -> (projT1 args))%ptype option
(fun x3 : option => x3)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -440,7 +440,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s0 -> (projT1 args0)) -> (projT1 args))%ptype option
(fun x3 : option => x3)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -490,7 +490,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args0) -> s) -> (projT1 args))%ptype option
(fun x3 : option => x3)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -540,7 +540,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s0 -> (projT1 args0)) -> (projT1 args))%ptype option
(fun x3 : option => x3)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -594,7 +594,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args1) -> s) -> (projT1 args) -> s1)%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, (_, _)) =>
+ | Some (_, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
@@ -666,7 +666,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s0 -> (projT1 args1)) -> (projT1 args) -> s1)%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, (_, _)) =>
+ | Some (_, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
@@ -737,7 +737,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args1) -> s) -> s2 -> (projT1 args))%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, (_, _)) =>
+ | Some (_, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
@@ -805,7 +805,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s0 -> (projT1 args1)) -> s2 -> (projT1 args))%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, (_, _)) =>
+ | Some (_, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
@@ -873,7 +873,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args1) -> s) -> s2 -> (projT1 args))%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, (_, _)) =>
+ | Some (_, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
@@ -932,7 +932,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s0 -> (projT1 args1)) -> s2 -> (projT1 args))%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, (_, _)) =>
+ | Some (_, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
@@ -988,7 +988,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s0 -> (projT1 args0)) -> (projT1 args))%ptype option
(fun x3 : option => x3)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -1018,7 +1018,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s0 -> (projT1 args0)) -> (projT1 args))%ptype option
(fun x3 : option => x3)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -1054,7 +1054,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s0 -> (projT1 args1)) -> (projT1 args) -> s1)%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, (_, _)) =>
+ | Some (_, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
@@ -1097,7 +1097,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s0 -> (projT1 args1)) -> s2 -> (projT1 args))%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, (_, _)) =>
+ | Some (_, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
@@ -1140,7 +1140,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((s0 -> (projT1 args1)) -> s2 -> (projT1 args))%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, (_, _)) =>
+ | Some (_, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
@@ -1227,7 +1227,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args1) -> ℤ) -> s0 -> (projT1 args))%ptype option
(fun x4 : option => x4)
with
- | Some (_, _, (_, _)) =>
+ | Some (_, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
@@ -1276,7 +1276,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args1) -> s0 -> (projT1 args)) -> ℤ)%ptype option
(fun x4 : option => x4)
with
- | Some (_, (_, _), _) =>
+ | Some (_, (_, _), _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ -> ℤ) -> ℤ)%ptype
@@ -1325,7 +1325,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args1) -> ℤ) -> s0 -> (projT1 args))%ptype option
(fun x4 : option => x4)
with
- | Some (_, _, (_, _)) =>
+ | Some (_, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
@@ -1374,7 +1374,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args1) -> s0 -> (projT1 args)) -> ℤ)%ptype option
(fun x4 : option => x4)
with
- | Some (_, (_, _), _) =>
+ | Some (_, (_, _), _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ -> ℤ) -> ℤ)%ptype
@@ -1418,7 +1418,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args) -> ℤ) -> ℤ)%ptype option
(fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype (((projT1 args) -> ℤ) -> ℤ)%ptype
@@ -1460,7 +1460,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((projT1 args1) -> ℤ) -> ℤ) -> s0 -> (projT1 args))%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, _, (_, _)) =>
+ | Some (_, _, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype
@@ -1510,7 +1510,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((projT1 args1) -> ℤ) -> s0 -> (projT1 args)) -> ℤ)%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, (_, _), _) =>
+ | Some (_, _, (_, _), _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype
@@ -1560,7 +1560,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((projT1 args1) -> ℤ) -> ℤ) -> s0 -> (projT1 args))%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, _, (_, _)) =>
+ | Some (_, _, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype
@@ -1610,7 +1610,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((projT1 args1) -> ℤ) -> s0 -> (projT1 args)) -> ℤ)%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, (_, _), _) =>
+ | Some (_, _, (_, _), _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ -> ℤ) -> ℤ)%ptype
@@ -1654,7 +1654,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((projT1 args) -> ℤ) -> ℤ) -> ℤ)%ptype option
(fun x3 : option => x3)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -1695,7 +1695,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args1) -> ℤ) -> s0 -> (projT1 args))%ptype
option (fun x4 : option => x4)
with
- | Some (_, _, (_, _)) =>
+ | Some (_, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
@@ -1733,7 +1733,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args1) -> ℤ) -> s0 -> (projT1 args))%ptype
option (fun x4 : option => x4)
with
- | Some (_, _, (_, _)) =>
+ | Some (_, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ -> ℤ)%ptype
@@ -1773,7 +1773,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args) -> ℤ) -> ℤ)%ptype option
(fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype (((projT1 args) -> ℤ) -> ℤ)%ptype
@@ -1813,7 +1813,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((projT1 args1) -> ℤ) -> ℤ) -> s0 -> (projT1 args))%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, _, (_, _)) =>
+ | Some (_, _, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype
@@ -1851,7 +1851,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((projT1 args1) -> ℤ) -> ℤ) -> s0 -> (projT1 args))%ptype
option (fun x5 : option => x5)
with
- | Some (_, _, _, (_, _)) =>
+ | Some (_, _, _, (_, _))%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ -> ℤ)%ptype
@@ -1891,7 +1891,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((projT1 args) -> ℤ) -> ℤ) -> ℤ)%ptype option
(fun x3 : option => x3)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -1930,7 +1930,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((projT1 args) -> s) -> ℤ) -> ℤ)%ptype option
(fun x4 : option => x4)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -1964,7 +1964,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((projT1 args) -> s) -> ℤ) -> ℤ)%ptype option
(fun x4 : option => x4)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -1995,7 +1995,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((s0 -> (projT1 args)) -> ℤ) -> ℤ)%ptype option
(fun x4 : option => x4)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -2030,7 +2030,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
((ℤ -> ℤ) -> ℤ)%ptype option (fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq ((ℤ -> ℤ) -> ℤ)%ptype
((ℤ -> ℤ) -> ℤ)%ptype
@@ -2046,7 +2046,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
pattern.type.unify_extracted_cps ((ℤ -> ℤ) -> ℤ)%ptype
((ℤ -> ℤ) -> ℤ)%ptype option (fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq ((ℤ -> ℤ) -> ℤ)%ptype
((ℤ -> ℤ) -> ℤ)%ptype
@@ -2068,7 +2068,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((projT1 args0) -> ℤ) -> ℤ) -> (projT1 args))%ptype option
(fun x3 : option => x3)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
diff --git a/src/Experiments/NewPipeline/nbe_rewrite_head.out b/src/Experiments/NewPipeline/nbe_rewrite_head.out
index f56e12da0..076992962 100644
--- a/src/Experiments/NewPipeline/nbe_rewrite_head.out
+++ b/src/Experiments/NewPipeline/nbe_rewrite_head.out
@@ -58,7 +58,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℕ -> ℕ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -93,7 +93,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℕ -> ℕ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -128,7 +128,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℕ -> ℕ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -163,7 +163,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℕ -> ℕ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -205,7 +205,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) ->
s0) -> s)%ptype option (fun x2 : option => x2)
with
- | Some (_, _, _, (_, (_, (_, _)), b3, b2)) =>
+ | Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange =>
if
type.type_beq base.type base.type.type_beq
(((b3 * b2)%etype -> b3) ->
@@ -256,7 +256,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((let (x2, _) := args in x2) * (let (_, y) := args in y))%etype) ->
s0) -> s)%ptype option (fun x2 : option => x2)
with
- | Some (_, _, _, (_, (_, (_, _)), b3, b2)) =>
+ | Some (_, _, _, (_, (_, (_, _)), b3, b2))%zrange =>
if
type.type_beq base.type base.type.type_beq
(((b3 * b2)%etype -> b2) ->
@@ -311,7 +311,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
s0) -> s)%ptype option (fun x3 : option => x3)
with
| Some
- (_, (_, _), (_, _, _), (_, (_, b7)), (_, (_, (_, _)), b9, b8)) =>
+ (_, (_, _), (_, _, _), (_, (_, b7)), (_, (_, (_, _)), b9, b8))%zrange =>
if
type.type_beq base.type base.type.type_beq
((((b9 -> b8 -> b7) -> (b9 * b8)%etype -> b7) ->
@@ -421,7 +421,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
unit -> T) -> (projT1 args))%ptype option
(fun x2 : option => x2)
with
- | Some (_, _, (_, _, (_, _)), (_, _), (_, b8), _) =>
+ | Some (_, _, (_, _, (_, _)), (_, _), (_, b8), _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((((unit -> b8) -> (unit -> b8) -> bool -> b8) ->
@@ -500,7 +500,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
ℕ -> P -> P) -> (projT1 args))%ptype option
(fun x2 : option => x2)
with
- | Some (_, _, (_, (_, _), (_, _)), (_, _), (_, (_, b10)), _) =>
+ | Some
+ (_, _, (_, (_, _), (_, _)), (_, _), (_, (_, b10)), _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((((unit -> b10) -> (ℕ -> b10 -> b10) -> ℕ -> b10) ->
@@ -633,7 +634,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
with
| Some
(_, _, (_, (_, _, (_, _)), (_, (_, _))), (_, _),
- (_, (_, _, (_, b16))), _, b) =>
+ (_, (_, _, (_, b16))), _, b)%zrange =>
if
type.type_beq base.type base.type.type_beq
((((((b -> b16) ->
@@ -884,7 +885,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(fun x2 : option => x2)
with
| Some
- (_, _, (_, (_, (_, _)), (_, _)), (_, _), (_, (_, (_, b12))), b) =>
+ (_, _, (_, (_, (_, _)), (_, _)), (_, _), (_, (_, (_, b12))), b)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((((unit -> b12) ->
@@ -1119,7 +1120,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
unit -> P) -> A -> (list A) -> P) -> (list args))%ptype
option (fun x2 : option => x2)
with
- | Some (_, _, (_, (_, _), (_, _)), (_, _), (_, (_, b10)), b) =>
+ | Some
+ (_, _, (_, (_, _), (_, _)), (_, _), (_, (_, b10)), b)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((((unit -> b10) ->
@@ -1241,7 +1243,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
with
| Some
(_, _, (_, (_, _), (_, _)), (_, _), (_, (_, b10)),
- (_, (_, _), _, b11)) =>
+ (_, (_, _), _, b11))%zrange =>
if
type.type_beq base.type base.type.type_beq
(((((unit -> b10) ->
@@ -1372,7 +1374,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((pattern.base.type.list '1) -> ℕ) -> (pattern.base.type.list '1))%ptype
(((list T) -> ℕ) -> (list T))%ptype option (fun x0 : option => x0)
with
- | Some (_, _, b) =>
+ | Some (_, _, b)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((list b) -> ℕ) -> (list b))%ptype
@@ -1400,7 +1402,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℕ -> ℕ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -1437,7 +1439,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((ℕ -> (list A) -> (list A)) -> (projT1 args)) -> (list A))%ptype
option (fun x1 : option => x1)
with
- | Some (_, (_, _), _, b) =>
+ | Some (_, (_, _), _, b)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℕ -> (list b) -> (list b)) -> ℕ) -> (list b))%ptype
@@ -1477,7 +1479,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((ℕ -> (list A) -> (list A)) -> (projT1 args)) -> (list A))%ptype
option (fun x1 : option => x1)
with
- | Some (_, (_, _), _, b) =>
+ | Some (_, (_, _), _, b)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℕ -> (list b) -> (list b)) -> ℕ) -> (list b))%ptype
@@ -1515,7 +1517,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
ℕ)%ptype (((A -> ℕ -> (list A)) -> A) -> (projT1 args))%ptype
option (fun x1 : option => x1)
with
- | Some (_, (_, _), b0, _) =>
+ | Some (_, (_, _), b0, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((b0 -> ℕ -> (list b0)) -> b0) -> ℕ)%ptype
@@ -1552,7 +1554,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((list A) -> (list B) -> (list (A * B))) -> (list A)) -> (list B))%ptype
option (fun x1 : option => x1)
with
- | Some (_, (_, (_, _)), b0, b) =>
+ | Some (_, (_, (_, _)), b0, b)%zrange =>
if
type.type_beq base.type base.type.type_beq
((((list b0) -> (list b) -> (list (b0 * b))) -> (list b0)) ->
@@ -1576,7 +1578,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
ys <- reflect_list (v0 x0);
Some
(Compilers.reify_list
- (map (fun '(x1, y) => (x1, y)%expr_pat)
+ (map (fun '(x1, y)%zrange => (x1, y)%expr_pat)
(combine xs ys))));
(trA <-- @base.try_make_transport_cps
(fun A0 : base.type => expr (list (A0 * B))) A A;
@@ -1619,7 +1621,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((A -> B) -> (list A) -> (list B)) -> A -> B) -> (list A))%ptype
option (fun x1 : option => x1)
with
- | Some (_, _, (_, _), (_, b4), b) =>
+ | 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
@@ -1742,7 +1744,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((list A) -> (list A) -> (list A)) -> (list A)) -> (list A))%ptype
option (fun x1 : option => x1)
with
- | Some (_, (_, _), _, b) =>
+ | Some (_, (_, _), _, b)%zrange =>
if
type.type_beq base.type base.type.type_beq
((((list b) -> (list b) -> (list b)) -> (list b)) -> (list b))%ptype
@@ -1794,7 +1796,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((list A) -> (list A)) -> (list A))%ptype option
(fun x0 : option => x0)
with
- | Some (_, _, b) =>
+ | Some (_, _, b)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((list b) -> (list b)) -> (list b))%ptype
@@ -1826,7 +1828,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((A -> (list B)) -> (list A) -> (list B)) -> A -> (list B)) ->
(list A))%ptype option (fun x1 : option => x1)
with
- | Some (_, _, (_, _), (_, b4), b) =>
+ | Some (_, _, (_, _), (_, b4), b)%zrange =>
if
type.type_beq base.type base.type.type_beq
((((b -> (list b4)) -> (list b) -> (list b4)) -> b -> (list b4)) ->
@@ -1930,7 +1932,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((A -> bool) -> (list A) -> (list A * list A)%etype) -> A -> bool) ->
(list A))%ptype option (fun x1 : option => x1)
with
- | Some (_, _, (_, (_, _)), (_, _), b) =>
+ | Some (_, _, (_, (_, _)), (_, _), b)%zrange =>
if
type.type_beq base.type base.type.type_beq
((((b -> bool) -> (list b) -> (list b * list b)%etype) ->
@@ -2165,7 +2167,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((((B -> A -> A) -> A -> (list B) -> A) -> B -> A -> A) -> A) ->
(list B))%ptype option (fun x2 : option => x2)
with
- | Some (_, (_, _), (_, (_, _)), (_, (_, _)), b0, b) =>
+ | Some (_, (_, _), (_, (_, _)), (_, (_, _)), b0, b)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((((b -> b0 -> b0) -> b0 -> (list b) -> b0) -> b -> b0 -> b0) ->
@@ -2315,7 +2317,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((ℕ -> (T -> T) -> (list T) -> (list T)) -> (projT1 args)) ->
T -> T) -> (list T))%ptype option (fun x2 : option => x2)
with
- | Some (_, (_, _, (_, _)), _, (_, _), b) =>
+ | Some (_, (_, _, (_, _)), _, (_, _), b)%zrange =>
if
type.type_beq base.type base.type.type_beq
((((ℕ -> (b -> b) -> (list b) -> (list b)) -> ℕ) -> b -> b) ->
@@ -2396,7 +2398,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((((T -> (list T) -> ℕ -> T) -> T) -> (list T)) ->
(projT1 args))%ptype option (fun x2 : option => x2)
with
- | Some (_, (_, (_, _)), _, b0, _) =>
+ | Some (_, (_, (_, _)), _, b0, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((((b0 -> (list b0) -> ℕ -> b0) -> b0) -> (list b0)) -> ℕ)%ptype
@@ -2437,7 +2439,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -2472,7 +2474,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -2507,7 +2509,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -2542,7 +2544,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -2598,7 +2600,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -2633,7 +2635,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -2711,7 +2713,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -2746,7 +2748,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -2781,7 +2783,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -2860,7 +2862,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -2895,7 +2897,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -2930,7 +2932,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -2965,7 +2967,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -3023,7 +3025,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -3062,7 +3064,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype
option (fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -3077,7 +3079,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
Some
(Base
(let
- '(a1, b1) :=
+ '(a1, b1)%zrange :=
Definitions.Z.mul_split
(let (x2, _) := idc_args in x2)
(let (x2, _) := idc_args0 in x2)
@@ -3110,7 +3112,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype
option (fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -3125,7 +3127,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
Some
(Base
(let
- '(a1, b1) :=
+ '(a1, b1)%zrange :=
Definitions.Z.add_get_carry_full
(let (x2, _) := idc_args in x2)
(let (x2, _) := idc_args0 in x2)
@@ -3158,7 +3160,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype
option (fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -3208,7 +3210,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(projT1 args0)) -> (projT1 args))%ptype option
(fun x3 : option => x3)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -3226,7 +3228,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
Some
(Base
(let
- '(a2, b2) :=
+ '(a2, b2)%zrange :=
Definitions.Z.add_with_get_carry_full
(let (x3, _) := idc_args in x3)
(let (x3, _) := idc_args0 in x3)
@@ -3262,7 +3264,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype
option (fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -3277,7 +3279,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
Some
(Base
(let
- '(a1, b1) :=
+ '(a1, b1)%zrange :=
Definitions.Z.sub_get_borrow_full
(let (x2, _) := idc_args in x2)
(let (x2, _) := idc_args0 in x2)
@@ -3315,7 +3317,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(projT1 args0)) -> (projT1 args))%ptype option
(fun x3 : option => x3)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -3333,7 +3335,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
Some
(Base
(let
- '(a2, b2) :=
+ '(a2, b2)%zrange :=
Definitions.Z.sub_with_get_borrow_full
(let (x3, _) := idc_args in x3)
(let (x3, _) := idc_args0 in x3)
@@ -3369,7 +3371,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype
option (fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -3414,7 +3416,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(((projT1 args1) -> (projT1 args0)) -> (projT1 args))%ptype
option (fun x2 : option => x2)
with
- | Some (_, _, _) =>
+ | Some (_, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((ℤ -> ℤ) -> ℤ)%ptype
@@ -3464,7 +3466,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(projT1 args0)) -> (projT1 args))%ptype option
(fun x3 : option => x3)
with
- | Some (_, _, _, _) =>
+ | Some (_, _, _, _)%zrange =>
if
type.type_beq base.type base.type.type_beq
(((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype
@@ -3512,7 +3514,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
((projT1 args0) -> (projT1 args))%ptype option
(fun x1 : option => x1)
with
- | Some (_, _) =>
+ | Some (_, _)%zrange =>
if
type.type_beq base.type base.type.type_beq (ℤ -> ℤ)%ptype
((projT1 args0) -> (projT1 args))%ptype
@@ -3589,7 +3591,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(projT1 args1)) -> (projT1 args0)) -> (projT1 args))%ptype
option (fun x4 : option => x4)
with
- | Some (_, _, (_, (_, _, _)), (_, (_, (_, _)), _, _), _) =>
+ | Some (_, _, (_, (_, _, _)), (_, (_, (_, _)), _, _), _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((((ℤ * ℤ)%etype -> ℤ -> (ℤ * ℤ * ℤ)%etype) ->
@@ -3616,7 +3618,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(##(fancy.interp (invert_Some (to_fancy fancy_selc))
(let (x4, _) := idc_args1 in x4,
let (x4, _) := idc_args2 in x4,
- let (x4, _) := idc_args3 in x4)%core))%expr)
+ let (x4, _) := idc_args3 in x4)%zrange))%expr)
else None
| None => None
end
@@ -3697,7 +3699,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(projT1 args1)) -> (projT1 args0)) -> (projT1 args))%ptype
option (fun x4 : option => x4)
with
- | Some (_, _, (_, (_, _, _)), (_, (_, (_, _)), _, _), _) =>
+ | Some (_, _, (_, (_, _, _)), (_, (_, (_, _)), _, _), _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((((ℤ * ℤ)%etype -> ℤ -> (ℤ * ℤ * ℤ)%etype) ->
@@ -3724,7 +3726,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(##(fancy.interp (invert_Some (to_fancy fancy_sell))
(let (x4, _) := idc_args1 in x4,
let (x4, _) := idc_args2 in x4,
- let (x4, _) := idc_args3 in x4)%core))%expr)
+ let (x4, _) := idc_args3 in x4)%zrange))%expr)
else None
| None => None
end
@@ -3802,7 +3804,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(projT1 args1)) -> (projT1 args0)) -> (projT1 args))%ptype
option (fun x4 : option => x4)
with
- | Some (_, _, (_, (_, _, _)), (_, (_, (_, _)), _, _), _) =>
+ | Some (_, _, (_, (_, _, _)), (_, (_, (_, _)), _, _), _)%zrange =>
if
type.type_beq base.type base.type.type_beq
((((ℤ * ℤ)%etype -> ℤ -> (ℤ * ℤ * ℤ)%etype) ->
@@ -3829,7 +3831,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with
(##(fancy.interp (invert_Some (to_fancy fancy_addm))
(let (x4, _) := idc_args1 in x4,
let (x4, _) := idc_args2 in x4,
- let (x4, _) := idc_args3 in x4)%core))%expr)
+ let (x4, _) := idc_args3 in x4)%zrange))%expr)
else None
| None => None
end
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 03:56:24 +0000