diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Language.v | 1 | ||||
| -rw-r--r-- | src/Rewriter.v | 2 | ||||
| -rw-r--r-- | src/RewriterRules.v | 52 | ||||
| -rw-r--r-- | src/RewriterRulesGood.v | 2 | ||||
| -rw-r--r-- | src/RewriterRulesInterpGood.v | 4 | ||||
| -rw-r--r-- | src/UnderLetsProofs.v | 367 | ||||
| -rw-r--r-- | src/arith_rewrite_head.out | 681 | ||||
| -rw-r--r-- | src/arith_with_casts_rewrite_head.out | 1229 | ||||
| -rw-r--r-- | src/fancy_rewrite_head.out | 63 | ||||
| -rw-r--r-- | src/fancy_with_casts_rewrite_head.out | 465 | ||||
| -rw-r--r-- | src/nbe_rewrite_head.out | 766 | ||||
| -rw-r--r-- | src/strip_literal_casts_rewrite_head.out | 67 |
12 files changed, 2542 insertions, 1157 deletions
diff --git a/src/Language.v b/src/Language.v index 2e29b4d77..eb400d704 100644 --- a/src/Language.v +++ b/src/Language.v @@ -1157,6 +1157,7 @@ Module Compilers. Notation LiteralZRange := (@Literal base.type.zrange). Definition literal {T} (v : T) := v. Definition eagerly {T} (v : T) := v. + Definition gets_inlined (real_val : bool) {T} (v : T) : bool := real_val. (** TODO: MOVE ME? *) Module Thunked. diff --git a/src/Rewriter.v b/src/Rewriter.v index 8b074aca6..770a7f391 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -2763,7 +2763,7 @@ Module Compilers. Definition RewriteNBE {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t := @Compile.Rewrite (@nbe_rewrite_head) nbe_default_fuel t e. Definition RewriteArith (max_const_val : Z) {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t - := @Compile.Rewrite (@arith_rewrite_head max_const_val) arith_default_fuel t e. + := @Compile.Rewrite (fun var do_again => @arith_rewrite_head max_const_val var) arith_default_fuel t e. Definition RewriteArithWithCasts {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t := @Compile.Rewrite (@arith_with_casts_rewrite_head) arith_with_casts_default_fuel t e. Definition RewriteStripLiteralCasts {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t diff --git a/src/RewriterRules.v b/src/RewriterRules.v index 4ded9846f..097497d9a 100644 --- a/src/RewriterRules.v +++ b/src/RewriterRules.v @@ -46,6 +46,49 @@ Local Notation "x <= y" := (is_tighter_than_bool (ZRange.normalize x) y = true) Local Notation litZZ x := (ident.literal (fst x), ident.literal (snd x)) (only parsing). Local Notation n r := (ZRange.normalize r) (only parsing). +Local Ltac generalize_cast' force_progress term := + let default _ := lazymatch force_progress with + | false => term + end in + lazymatch type of term with + | Prop => lazymatch term with + | context[ident.cast_outside_of_range] + => lazymatch (eval pattern ident.cast_outside_of_range in term) with + | (fun x : ?T => ?f) _ + => constr:(forall x : T, f) + end + | _ => default () + end + | _ + => lazymatch term with + | context[ident.cast_outside_of_range] + => let term := match term with + | context F[@cons Prop ?x] + => let x := generalize_cast' true x in + let term := context F[@cons Prop x] in + term + | context F[@cons (?T * Prop) (?b, ?x)] + => let x := generalize_cast' true x in + let term := context F[@cons (T * Prop) (b, x)] in + term + end in + generalize_cast' false term + | _ => default () + end + end. +Local Ltac generalize_cast term := generalize_cast' false term. + +(* Play tricks/games with [match] to get [term] interpreted as a constr rather than an ident when it's not closed, to get better error messages *) +Local Notation generalize_cast term + := (match term return _ with + | _TERM => ltac:(let TERM := (eval cbv delta [_TERM] in _TERM) in + let res := generalize_cast TERM in + exact res) + end) (only parsing). + +Local Notation myflatten_generalize_cast x + := (myflatten (generalize_cast x)) (only parsing). + (* N.B. [ident.eagerly] does not play well with [do_again] *) Definition nbe_rewrite_rulesT : list (bool * Prop) := Eval cbv [myapp mymap myflatten] in @@ -276,16 +319,11 @@ Definition arith_rewrite_rulesT (max_const_val : Z) : list (bool * Prop) Z.add_with_get_carry_full s (- c) x (- y) = dlet vb := Z.sub_with_get_borrow_full s c x y in (fst vb, - snd vb)) ] - ; mymap - do_again - [ (* [do_again], so that if one of the arguments is concrete, we automatically get the rewrite rule for [Z_cast] applying to it *) - (forall r x y, cstZZ r (x, y) = (cstZ (fst r) x, cstZ (snd r) y)) - ] ]. Definition arith_with_casts_rewrite_rulesT : list (bool * Prop) := Eval cbv [myapp mymap myflatten] in - myflatten + myflatten_generalize_cast [mymap dont_do_again [(forall A B x y, @fst A B (x, y) = x) @@ -470,7 +508,7 @@ Section fancy. Definition fancy_with_casts_rewrite_rulesT : list (bool * Prop) := Eval cbv [myapp mymap myflatten] in - myflatten + myflatten_generalize_cast [mymap dont_do_again [(* diff --git a/src/RewriterRulesGood.v b/src/RewriterRulesGood.v index 935a32474..c4486ef67 100644 --- a/src/RewriterRulesGood.v +++ b/src/RewriterRulesGood.v @@ -52,7 +52,7 @@ Module Compilers. = @fancy_rewrite_head0. Proof. reflexivity. Qed. - Lemma arith_rewrite_head_eq max_const_val : @arith_rewrite_head max_const_val = (fun var => @arith_rewrite_head0 var max_const_val). + Lemma arith_rewrite_head_eq max_const_val : (fun var do_again => @arith_rewrite_head max_const_val var) = (fun var => @arith_rewrite_head0 var max_const_val). Proof. reflexivity. Qed. Lemma fancy_with_casts_rewrite_head_eq invert_low invert_high value_range flag_range diff --git a/src/RewriterRulesInterpGood.v b/src/RewriterRulesInterpGood.v index d30366220..c73867339 100644 --- a/src/RewriterRulesInterpGood.v +++ b/src/RewriterRulesInterpGood.v @@ -144,7 +144,7 @@ Module Compilers. | [ |- _ /\ _ ] => split; [ intros; exact I | ] end | progress cbn [eq_rect] in * ]; - cbn [fst snd base.interp base.base_interp type.interp projT1 projT2 UnderLets.interp expr.interp type.related ident.gen_interp UnderLets.interp_related] in *. + cbn [fst snd base.interp base.base_interp type.interp projT1 projT2 UnderLets.interp expr.interp type.related ident.gen_interp UnderLets.interp_related UnderLets.interp_related_gen] in *. Ltac recurse_interp_related_step := let do_replace v := @@ -350,7 +350,7 @@ Module Compilers. | ] | [ |- context[match _ with nil => _ | _ => _ end] ] => progress recursive_match_to_list_case_in_goal end - | progress cbn [expr.interp ident.gen_interp fst snd Compile.reify Compile.reflect Compile.wf_value' Compile.value' Option.bind UnderLets.interp list_case type.interp base.interp base.base_interp ident.to_fancy invert_Some ident.fancy.interp ident.fancy.interp_with_wordmax Compile.reify_expr bool_rect UnderLets.interp_related type.related] in * + | progress cbn [expr.interp ident.gen_interp fst snd Compile.reify Compile.reflect Compile.wf_value' Compile.value' Option.bind UnderLets.interp list_case type.interp base.interp base.base_interp ident.to_fancy invert_Some ident.fancy.interp ident.fancy.interp_with_wordmax Compile.reify_expr bool_rect UnderLets.interp_related UnderLets.interp_related_gen type.related] in * | progress cbv [Compile.option_bind' respectful expr.interp_related] in * | progress fold (@type.interp _ base.interp) | progress fold (@base.interp) diff --git a/src/UnderLetsProofs.v b/src/UnderLetsProofs.v index 54aee6d76..ccb872a44 100644 --- a/src/UnderLetsProofs.v +++ b/src/UnderLetsProofs.v @@ -501,88 +501,62 @@ Module Compilers. Qed. End with_var2. - Section for_interp. + Section for_interp2. Context {base_interp : base_type -> Type} - (ident_interp : forall t, ident t -> type.interp base_interp t). - - Local Notation UnderLets := (@UnderLets (type.interp base_interp)). + (ident_interp : forall t, ident t -> type.interp base_interp t) + {var : type -> Type}. - Fixpoint interp {T} (v : UnderLets T) : T - := match v with - | Base v => v - | UnderLet A x f => let xv := expr.interp ident_interp x in - @interp _ (f xv) - end. - - Fixpoint interp_related {T1 T2} (R : T1 -> T2 -> Prop) (e : UnderLets T1) (v2 : T2) : Prop + Fixpoint interp_related_gen {T1 T2} (R' : forall t, var t -> type.interp base_interp t -> Prop) (R : T1 -> T2 -> Prop) (e : @UnderLets var T1) (v2 : T2) : Prop := match e with | Base v1 => R v1 v2 | UnderLet t e f (* combine the App rule with the Abs rule *) => exists fv ev, - expr.interp_related ident_interp e ev + expr.interp_related_gen ident_interp R' e ev /\ (forall x1 x2, - x1 == x2 - -> @interp_related T1 T2 R (f x1) (fv x2)) + R' _ x1 x2 + -> @interp_related_gen T1 T2 R' R (f x1) (fv x2)) /\ fv ev = v2 end. - Lemma interp_splice {A B} (x : UnderLets A) (e : A -> UnderLets B) - : interp (splice x e) = interp (e (interp x)). - Proof. induction x; cbn [splice interp]; eauto. Qed. - - Lemma interp_splice_list {A B} (x : list (UnderLets A)) (e : list A -> UnderLets B) - : interp (splice_list x e) - = interp (e (List.map interp x)). - Proof. - revert e; induction x as [|x xs IHx]; intros; cbn [splice_list interp List.map]; [ reflexivity | ]. - rewrite interp_splice, IHx; reflexivity. - Qed. - - Lemma interp_to_expr {t} (x : UnderLets (expr t)) - : expr.interp ident_interp (to_expr x) = expr.interp ident_interp (interp x). - Proof. induction x; cbn [expr.interp interp to_expr]; cbv [LetIn.Let_In]; eauto. Qed. - - Lemma interp_of_expr {t} (x : expr t) - : expr.interp ident_interp (interp (of_expr x)) = expr.interp ident_interp x. - Proof. induction x; cbn [expr.interp interp of_expr]; cbv [LetIn.Let_In]; eauto. Qed. - - Lemma to_expr_interp_related_iff {t e v} - : interp_related (expr.interp_related ident_interp (t:=t)) e v - <-> expr.interp_related ident_interp (UnderLets.to_expr e) v. + Lemma to_expr_interp_related_gen_iff (R : forall t, var t -> type.interp base_interp t -> Prop) {t e v} + : interp_related_gen R (expr.interp_related_gen ident_interp R (t:=t)) e v + <-> expr.interp_related_gen ident_interp R (UnderLets.to_expr e) v. Proof using Type. - revert v; induction e; cbn [UnderLets.to_expr interp_related expr.interp_related]; try reflexivity. + revert v; induction e; cbn [UnderLets.to_expr interp_related_gen expr.interp_related_gen]; try reflexivity. setoid_rewrite H. reflexivity. Qed. - Global Instance interp_related_Proper_iff {T1 T2} - : Proper (pointwise_relation _ (pointwise_relation _ iff) ==> eq ==> eq ==> iff) (@interp_related T1 T2) | 10. + Global Instance interp_related_gen_Proper_iff {T1 T2 R} + : Proper (pointwise_relation _ (pointwise_relation _ iff) ==> eq ==> eq ==> iff) (@interp_related_gen T1 T2 R) | 10. Proof using Type. cbv [pointwise_relation respectful Proper]. intros R1 R2 HR x y ? x' y' H'; subst y y'. - revert x'; induction x; [ apply HR | ]; cbn [interp_related]. + revert x'; induction x; [ apply HR | ]; cbn [interp_related_gen]. setoid_rewrite H; reflexivity. Qed. - Lemma splice_interp_related_iff {A B T R x e} {v : T} - : interp_related R (@UnderLets.splice _ ident _ A B x e) v - <-> interp_related - (fun xv => interp_related R (e xv)) + Lemma splice_interp_related_gen_iff {A B T R' R x e} {v : T} + : interp_related_gen R' R (@UnderLets.splice _ ident _ A B x e) v + <-> interp_related_gen + R' + (fun xv => interp_related_gen R' R (e xv)) x v. Proof using Type. - revert v; induction x; cbn [UnderLets.splice interp_related]; [ reflexivity | ]. + revert v; induction x; cbn [UnderLets.splice interp_related_gen]; [ reflexivity | ]. match goal with H : _ |- _ => setoid_rewrite H end. reflexivity. Qed. - Lemma splice_list_interp_related_iff_gen {A B T R x e1 e2 base} {v : T} + Lemma splice_list_interp_related_gen_iff_gen {A B T R' R x e1 e2 base} {v : T} (He1e2 : forall ls', e1 ls' = e2 (base ++ ls')) - : interp_related R (@UnderLets.splice_list _ ident _ A B x e1) v + : interp_related_gen R' R (@UnderLets.splice_list _ ident _ A B x e1) v <-> list_rect (fun _ => list _ -> _ -> Prop) - (fun ls v => interp_related R (e2 ls) v) + (fun ls v => interp_related_gen R' R (e2 ls) v) (fun x xs recP ls v - => interp_related + => interp_related_gen + R' (fun x' v => recP (ls ++ [x']) v) x v) @@ -590,22 +564,23 @@ Module Compilers. base v. Proof using Type. - revert base v e1 e2 He1e2; induction x as [|? ? IHx]; cbn [UnderLets.splice_list interp_related list_rect]; intros. + revert base v e1 e2 He1e2; induction x as [|? ? IHx]; cbn [UnderLets.splice_list interp_related_gen list_rect]; intros. { intros; rewrite He1e2, ?app_nil_r; reflexivity. } - { setoid_rewrite splice_interp_related_iff. - apply interp_related_Proper_iff; [ | reflexivity.. ]; cbv [pointwise_relation]; intros. + { setoid_rewrite splice_interp_related_gen_iff. + apply interp_related_gen_Proper_iff; [ | reflexivity.. ]; cbv [pointwise_relation]; intros. specialize (fun v => IHx (base ++ [v])). setoid_rewrite IHx; [ reflexivity | ]. intros; rewrite He1e2, <- ?app_assoc; reflexivity. } Qed. - Lemma splice_list_interp_related_iff {A B T R x e} {v : T} - : interp_related R (@UnderLets.splice_list _ ident _ A B x e) v + Lemma splice_list_interp_related_gen_iff {A B T R' R x e} {v : T} + : interp_related_gen R' R (@UnderLets.splice_list _ ident _ A B x e) v <-> list_rect (fun _ => list _ -> _ -> Prop) - (fun ls v => interp_related R (e ls) v) + (fun ls v => interp_related_gen R' R (e ls) v) (fun x xs recP ls v - => interp_related + => interp_related_gen + R' (fun x' v => recP (ls ++ [x']) v) x v) @@ -613,19 +588,19 @@ Module Compilers. nil v. Proof using Type. - apply splice_list_interp_related_iff_gen; reflexivity. + apply splice_list_interp_related_gen_iff_gen; reflexivity. Qed. - Lemma splice_interp_related_of_ex {A B T T' RA RB x e} {v : T} + Lemma splice_interp_related_gen_of_ex {A B T T' R' RA RB x e} {v : T} : (exists ev (xv : T'), - interp_related RA x xv + interp_related_gen R' RA x xv /\ (forall x1 x2, RA x1 x2 - -> interp_related RB (e x1) (ev x2)) + -> interp_related_gen R' RB (e x1) (ev x2)) /\ ev xv = v) - -> interp_related RB (@UnderLets.splice _ ident _ A B x e) v. + -> interp_related_gen R' RB (@UnderLets.splice _ ident _ A B x e) v. Proof using Type. - revert e v; induction x; cbn [interp_related UnderLets.splice]; intros. + revert e v; induction x; cbn [interp_related_gen UnderLets.splice]; intros. all: repeat first [ progress destruct_head'_ex | progress destruct_head'_and | progress subst @@ -635,21 +610,21 @@ Module Compilers. end ]. do 2 eexists; repeat apply conj; [ eassumption | | ]; intros. { match goal with H : _ |- _ => apply H; clear H end. - do 2 eexists; repeat apply conj; now eauto. } + do 2 eexists; repeat apply conj; try now eauto. } { reflexivity. } Qed. - Lemma splice_list_interp_related_of_ex {A B T T' RA RB x e} {v : T} + Lemma splice_list_interp_related_gen_of_ex {A B T T' R' RA RB x e} {v : T} : (exists ev (xv : list T'), - List.Forall2 (interp_related RA) x xv + List.Forall2 (interp_related_gen R' RA) x xv /\ (forall x1 x2, List.length x2 = List.length xv -> List.Forall2 RA x1 x2 - -> interp_related RB (e x1) (ev x2)) + -> interp_related_gen R' RB (e x1) (ev x2)) /\ ev xv = v) - -> interp_related RB (@UnderLets.splice_list _ ident _ A B x e) v. + -> interp_related_gen R' RB (@UnderLets.splice_list _ ident _ A B x e) v. Proof using Type. - revert e v; induction x as [|x xs IHxs]; cbn [interp_related UnderLets.splice_list]; intros. + revert e v; induction x as [|x xs IHxs]; cbn [interp_related_gen UnderLets.splice_list]; intros. all: repeat first [ progress destruct_head'_ex | progress destruct_head'_and | progress cbn [List.length] in * @@ -665,7 +640,7 @@ Module Compilers. | [ H : forall l1 l2, length l2 = S (length _) -> Forall2 _ l1 l2 -> _ |- _ ] => specialize (fun l ls l' ls' (pf0 : length _ = _) pf1 pf2 => H (cons l ls) (cons l' ls') (f_equal S pf0) (Forall2_cons _ _ pf1 pf2)) end. - eapply splice_interp_related_of_ex; do 2 eexists; repeat apply conj; + eapply splice_interp_related_gen_of_ex; do 2 eexists; repeat apply conj; intros; [ eassumption | | ]. { eapply IHxs. do 2 eexists; repeat apply conj; intros; @@ -675,6 +650,207 @@ Module Compilers. { reflexivity. } Qed. + Lemma list_rect_interp_related_gen {A B Pnil Pcons ls B' Pnil' Pcons' ls' R' R} + (Hnil : interp_related_gen R' R Pnil Pnil') + (Hcons : forall x x', + expr.interp_related_gen ident_interp R' x x' + -> forall l l', + List.Forall2 (expr.interp_related_gen ident_interp R') l l' + -> forall rec rec', + interp_related_gen R' R rec rec' + -> interp_related_gen R' R (Pcons x l rec) (Pcons' x' l' rec')) + (Hls : List.Forall2 (expr.interp_related_gen ident_interp R' (t:=A)) ls ls') + : interp_related_gen + R' R + (list_rect + (fun _ : list _ => UnderLets _ B) + Pnil + Pcons + ls) + (list_rect + (fun _ : list _ => B') + Pnil' + Pcons' + ls'). + Proof using Type. induction Hls; cbn [list_rect] in *; auto. Qed. + + Lemma list_rect_arrow_interp_related_gen {A B C Pnil Pcons ls x B' C' Pnil' Pcons' ls' x' R'' R} + {R' : B -> B' -> Prop} + (Hnil : forall x x', R' x x' -> interp_related_gen R'' R (Pnil x) (Pnil' x')) + (Hcons : forall x x', + expr.interp_related_gen ident_interp R'' x x' + -> forall l l', + List.Forall2 (expr.interp_related_gen ident_interp R'') l l' + -> forall rec rec', + (forall v v', R' v v' -> interp_related_gen R'' R (rec v) (rec' v')) + -> forall v v', + R' v v' + -> interp_related_gen R'' R (Pcons x l rec v) (Pcons' x' l' rec' v')) + (Hls : List.Forall2 (expr.interp_related_gen ident_interp R'' (t:=A)) ls ls') + (Hx : R' x x') + : interp_related_gen + R'' R + (list_rect + (fun _ : list _ => B -> UnderLets _ C) + Pnil + Pcons + ls + x) + (list_rect + (fun _ : list _ => B' -> C') + Pnil' + Pcons' + ls' + x'). + Proof using Type. revert x x' Hx; induction Hls; cbn [list_rect] in *; auto. Qed. + + Lemma nat_rect_interp_related_gen {A PO PS n A' PO' PS' n' R' R} + (Hnil : interp_related_gen R' R PO PO') + (Hcons : forall n rec rec', + interp_related_gen R' R rec rec' + -> interp_related_gen R' R (PS n rec) (PS' n rec')) + (Hn : n = n') + : interp_related_gen + R' R + (nat_rect (fun _ => UnderLets _ A) PO PS n) + (nat_rect (fun _ => A') PO' PS' n'). + Proof using Type. subst n'; induction n; cbn [nat_rect] in *; auto. Qed. + + Lemma nat_rect_arrow_interp_related_gen {A B PO PS n x A' B' PO' PS' n' x' R'' R} + {R' : A -> A' -> Prop} + (Hnil : forall x x', R' x x' -> interp_related_gen R'' R (PO x) (PO' x')) + (Hcons : forall n rec rec', + (forall x x', R' x x' -> interp_related_gen R'' R (rec x) (rec' x')) + -> forall x x', + R' x x' + -> interp_related_gen R'' R (PS n rec x) (PS' n rec' x')) + (Hn : n = n') + (Hx : R' x x') + : interp_related_gen + R'' R + (nat_rect (fun _ => A -> UnderLets _ B) PO PS n x) + (nat_rect (fun _ => A' -> B') PO' PS' n' x'). + Proof using Type. subst n'; revert x x' Hx; induction n; cbn [nat_rect] in *; auto. Qed. + + Lemma interp_related_gen_Proper_impl_same_UnderLets {A B B' R' R1 R2 e v f} + (HR : forall e v, (R1 e v : Prop) -> (R2 e (f v) : Prop)) + : @interp_related_gen A B R' R1 e v + -> @interp_related_gen A B' R' R2 e (f v). + Proof using Type. + revert f v HR; induction e; cbn [interp_related_gen]; [ now eauto | ]; intros F v HR H'. + destruct H' as [fv H']; exists (fun ev => F (fv ev)). + repeat first [ let x := fresh "x" in destruct H' as [x H']; exists x + | let x := fresh "x" in intro x; specialize (H' x) + | let H := fresh "H" in destruct H' as [H H']; split; [ exact H || now subst | ] + | let H := fresh "H" in destruct H' as [H' H]; split; [ | exact H || now subst ] ]. + auto. + Qed. + End for_interp2. + + Section for_interp. + Context {base_interp : base_type -> Type} + (ident_interp : forall t, ident t -> type.interp base_interp t). + + Local Notation UnderLets := (@UnderLets (type.interp base_interp)). + + Fixpoint interp {T} (v : UnderLets T) : T + := match v with + | Base v => v + | UnderLet A x f => let xv := expr.interp ident_interp x in + @interp _ (f xv) + end. + + Definition interp_related {T1 T2} (R : T1 -> T2 -> Prop) (e : UnderLets T1) (v2 : T2) : Prop + := @interp_related_gen base_interp ident_interp _ T1 T2 (fun t => type.eqv) R e v2. + + Lemma interp_splice {A B} (x : UnderLets A) (e : A -> UnderLets B) + : interp (splice x e) = interp (e (interp x)). + Proof. induction x; cbn [splice interp]; eauto. Qed. + + Lemma interp_splice_list {A B} (x : list (UnderLets A)) (e : list A -> UnderLets B) + : interp (splice_list x e) + = interp (e (List.map interp x)). + Proof. + revert e; induction x as [|x xs IHx]; intros; cbn [splice_list interp List.map]; [ reflexivity | ]. + rewrite interp_splice, IHx; reflexivity. + Qed. + + Lemma interp_to_expr {t} (x : UnderLets (expr t)) + : expr.interp ident_interp (to_expr x) = expr.interp ident_interp (interp x). + Proof. induction x; cbn [expr.interp interp to_expr]; cbv [LetIn.Let_In]; eauto. Qed. + + Lemma interp_of_expr {t} (x : expr t) + : expr.interp ident_interp (interp (of_expr x)) = expr.interp ident_interp x. + Proof. induction x; cbn [expr.interp interp of_expr]; cbv [LetIn.Let_In]; eauto. Qed. + + Lemma to_expr_interp_related_iff {t e v} + : interp_related (expr.interp_related ident_interp (t:=t)) e v + <-> expr.interp_related ident_interp (UnderLets.to_expr e) v. + Proof using Type. apply to_expr_interp_related_gen_iff. Qed. + + Global Instance interp_related_Proper_iff {T1 T2} + : Proper (pointwise_relation _ (pointwise_relation _ iff) ==> eq ==> eq ==> iff) (@interp_related T1 T2) | 10. + Proof using Type. apply interp_related_gen_Proper_iff. Qed. + + Lemma splice_interp_related_iff {A B T R x e} {v : T} + : interp_related R (@UnderLets.splice _ ident _ A B x e) v + <-> interp_related + (fun xv => interp_related R (e xv)) + x v. + Proof using Type. apply splice_interp_related_gen_iff. Qed. + + Lemma splice_list_interp_related_iff_gen {A B T R x e1 e2 base} {v : T} + (He1e2 : forall ls', e1 ls' = e2 (base ++ ls')) + : interp_related R (@UnderLets.splice_list _ ident _ A B x e1) v + <-> list_rect + (fun _ => list _ -> _ -> Prop) + (fun ls v => interp_related R (e2 ls) v) + (fun x xs recP ls v + => interp_related + (fun x' v => recP (ls ++ [x']) v) + x + v) + x + base + v. + Proof using Type. now apply splice_list_interp_related_gen_iff_gen. Qed. + + Lemma splice_list_interp_related_iff {A B T R x e} {v : T} + : interp_related R (@UnderLets.splice_list _ ident _ A B x e) v + <-> list_rect + (fun _ => list _ -> _ -> Prop) + (fun ls v => interp_related R (e ls) v) + (fun x xs recP ls v + => interp_related + (fun x' v => recP (ls ++ [x']) v) + x + v) + x + nil + v. + Proof using Type. apply splice_list_interp_related_gen_iff. Qed. + + Lemma splice_interp_related_of_ex {A B T T' RA RB x e} {v : T} + : (exists ev (xv : T'), + interp_related RA x xv + /\ (forall x1 x2, + RA x1 x2 + -> interp_related RB (e x1) (ev x2)) + /\ ev xv = v) + -> interp_related RB (@UnderLets.splice _ ident _ A B x e) v. + Proof using Type. apply splice_interp_related_gen_of_ex. Qed. + + Lemma splice_list_interp_related_of_ex {A B T T' RA RB x e} {v : T} + : (exists ev (xv : list T'), + List.Forall2 (interp_related RA) x xv + /\ (forall x1 x2, + List.length x2 = List.length xv + -> List.Forall2 RA x1 x2 + -> interp_related RB (e x1) (ev x2)) + /\ ev xv = v) + -> interp_related RB (@UnderLets.splice_list _ ident _ A B x e) v. + Proof using Type. apply splice_list_interp_related_gen_of_ex. Qed. + Lemma list_rect_interp_related {A B Pnil Pcons ls B' Pnil' Pcons' ls' R} (Hnil : interp_related R Pnil Pnil') (Hcons : forall x x', @@ -697,7 +873,7 @@ Module Compilers. Pnil' Pcons' ls'). - Proof using Type. induction Hls; cbn [list_rect] in *; auto. Qed. + Proof using Type. now apply list_rect_interp_related_gen. Qed. Lemma list_rect_arrow_interp_related {A B C Pnil Pcons ls x B' C' Pnil' Pcons' ls' x' R} {R' : B -> B' -> Prop} @@ -727,7 +903,7 @@ Module Compilers. Pcons' ls' x'). - Proof using Type. revert x x' Hx; induction Hls; cbn [list_rect] in *; auto. Qed. + Proof using Type. eapply list_rect_arrow_interp_related_gen; now eauto. Qed. Lemma nat_rect_interp_related {A PO PS n A' PO' PS' n' R} (Hnil : interp_related R PO PO') @@ -739,7 +915,7 @@ Module Compilers. R (nat_rect (fun _ => UnderLets A) PO PS n) (nat_rect (fun _ => A') PO' PS' n'). - Proof using Type. subst n'; induction n; cbn [nat_rect] in *; auto. Qed. + Proof using Type. now apply nat_rect_interp_related_gen. Qed. Lemma nat_rect_arrow_interp_related {A B PO PS n x A' B' PO' PS' n' x' R} {R' : A -> A' -> Prop} @@ -755,21 +931,13 @@ Module Compilers. R (nat_rect (fun _ => A -> UnderLets B) PO PS n x) (nat_rect (fun _ => A' -> B') PO' PS' n' x'). - Proof using Type. subst n'; revert x x' Hx; induction n; cbn [nat_rect] in *; auto. Qed. + Proof using Type. eapply nat_rect_arrow_interp_related_gen; now eauto. Qed. Lemma interp_related_Proper_impl_same_UnderLets {A B B' R1 R2 e v f} (HR : forall e v, (R1 e v : Prop) -> (R2 e (f v) : Prop)) : @interp_related A B R1 e v -> @interp_related A B' R2 e (f v). - Proof using Type. - revert f v HR; induction e; cbn [interp_related]; [ now eauto | ]; intros F v HR H'. - destruct H' as [fv H']; exists (fun ev => F (fv ev)). - repeat first [ let x := fresh "x" in destruct H' as [x H']; exists x - | let x := fresh "x" in intro x; specialize (H' x) - | let H := fresh "H" in destruct H' as [H H']; split; [ exact H || now subst | ] - | let H := fresh "H" in destruct H' as [H' H]; split; [ | exact H || now subst ] ]. - auto. - Qed. + Proof using Type. now apply interp_related_gen_Proper_impl_same_UnderLets. Qed. End for_interp. Section for_interp2. @@ -790,6 +958,37 @@ Module Compilers. eassumption. Qed. End for_interp2. + + Section with_var2_for_interp. + Context {base_interp : base_type -> Type} + {ident_interp : forall t, ident t -> type.interp base_interp t} + {var1 var2 : type -> Type}. + + Lemma flat_map_interp_related_iff + {T1 T2} f f' R'' R' R e v + (Hf : forall t e v, expr.interp_related_gen ident_interp R'' e v -> interp_related_gen ident_interp R' (expr.interp_related_gen ident_interp R') (f t e) v) + (Hf' : forall t e v, R' t e v -> R'' t (f' t e) v) + (He : @interp_related_gen _ ident_interp _ _ _ R'' R e v) + : @interp_related_gen + _ ident_interp _ _ T2 R' R + (@flat_map _ ident var1 ident var2 f f' T1 e) + v. + Proof using Type. + revert dependent v; induction e as [|? ? ? IHe]; cbn [flat_map interp_related_gen] in *; intros; [ assumption | ]. + repeat first [ progress destruct_head'_ex + | progress destruct_head'_and + | progress subst + | eapply splice_interp_related_gen_of_ex; do 2 eexists; repeat apply conj; + [ eapply Hf | | reflexivity ] + | solve [ auto ] + | progress intros + | match goal with + | [ |- interp_related_gen _ _ _ (UnderLet _ _) _ ] + => cbn [interp_related_gen]; do 2 eexists; repeat apply conj; + [ | | reflexivity ] + end ]. + Qed. + End with_var2_for_interp. End with_ident. Section reify. diff --git a/src/arith_rewrite_head.out b/src/arith_rewrite_head.out index e2755de01..1d3591c3b 100644 --- a/src/arith_rewrite_head.out +++ b/src/arith_rewrite_head.out @@ -47,7 +47,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with _ <- 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 (Base (v4 (v3 (v1 (v (Compile.reflect x1)))))) + 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 @@ -100,7 +104,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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 (Base (v4 (v3 (v2 (v0 (Compile.reflect x0)))))) + 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 @@ -151,6 +159,26 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with to_expr (x0 ($x3) (fun x6 : expr P => Base ($x4 @ x6)%expr_pat) ($x5)))%expr @ x1 @ x2)%expr_pat +| @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)) @@ -160,6 +188,43 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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 +| @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 + (#(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 +| @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)) @@ -218,6 +283,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | @List_nth_default T => fun (x : expr T) (x0 : expr (list T)) (x1 : expr ℕ) => Base (#(List_nth_default)%expr @ x @ x0 @ x1)%expr_pat +| @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 @@ -234,7 +302,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (if (let (x1, _) := xv in x1) =? 0 - then Datatypes.Some (Base x0) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x0)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -257,7 +329,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (if (let (x1, _) := xv in x1) =? 0 - then Datatypes.Some (Base x) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -280,9 +356,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s0 ℤ; v0 <- type.try_make_transport_cps s ℤ; Datatypes.Some - (Base - (- - (v (Compile.reflect x2) + v0 (Compile.reflect x1)))%expr) + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (- + ($(v (Compile.reflect x2)) + + $(v0 (Compile.reflect x1)))); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end @@ -309,7 +388,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (s -> ℤ)%ptype then v <- type.try_make_transport_cps s ℤ; - Datatypes.Some (Base (x0 - v (Compile.reflect x1))%expr) + Datatypes.Some + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x0 - $(v (Compile.reflect x1))); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end @@ -338,9 +421,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if (let (x2, _) := xv in x2) >? 0 then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false (##(let (x2, _) := xv in x2) - - v (Compile.reflect x1))%expr) + $(v (Compile.reflect x1)))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -363,10 +447,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if (let (x2, _) := xv in x2) <? 0 then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false (- - (v (Compile.reflect x1) + - ##(- (let (x2, _) := xv in x2))%Z))%expr) + ($(v (Compile.reflect x1)) + + ##(- (let (x2, _) := xv in x2))%Z))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -390,7 +475,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ℤ -> s)%ptype then v <- type.try_make_transport_cps s ℤ; - Datatypes.Some (Base (x - v (Compile.reflect x1))%expr) + Datatypes.Some + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x - $(v (Compile.reflect x1))); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end);; @@ -412,9 +501,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if (let (x2, _) := xv in x2) >? 0 then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false (##(let (x2, _) := xv in x2) - - v (Compile.reflect x1))%expr) + $(v (Compile.reflect x1)))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -437,10 +527,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if (let (x2, _) := xv in x2) <? 0 then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false (- (##(- (let (x2, _) := xv in x2))%Z + - v (Compile.reflect x1)))%expr) + $(v (Compile.reflect x1))))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -472,7 +563,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (if (let (x1, _) := xv in x1) =? 0 - then Datatypes.Some (Base (##0)%expr) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false ##0) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -495,7 +589,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (if (let (x1, _) := xv in x1) =? 0 - then Datatypes.Some (Base (##0)%expr) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false ##0) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -518,7 +615,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (if (let (x1, _) := xv in x1) =? 1 - then Datatypes.Some (Base x0) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x0)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -541,7 +642,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (if (let (x1, _) := xv in x1) =? 1 - then Datatypes.Some (Base x) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -565,7 +670,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args0); fv <- (if (let (x2, _) := xv in x2) =? -1 then - Datatypes.Some (Base (v (Compile.reflect x1))) + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($(v (Compile.reflect x1)))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -596,7 +704,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s ℤ; fv <- (if (let (x2, _) := xv in x2) =? -1 then - Datatypes.Some (Base (v (Compile.reflect x1))) + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($(v (Compile.reflect x1)))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -624,7 +735,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (if (let (x1, _) := xv in x1) =? -1 - then Datatypes.Some (Base (- x0)%expr) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (- $x0)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -647,7 +762,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (if (let (x1, _) := xv in x1) =? -1 - then Datatypes.Some (Base (- x)%expr) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (- $x)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -670,8 +789,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s0 ℤ; v0 <- type.try_make_transport_cps s ℤ; Datatypes.Some - (Base - (v (Compile.reflect x2) * v0 (Compile.reflect x1))%expr) + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($(v (Compile.reflect x2)) * + $(v0 (Compile.reflect x1))); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end @@ -698,7 +820,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (s -> ℤ)%ptype then v <- type.try_make_transport_cps s ℤ; - Datatypes.Some (Base (- (v (Compile.reflect x1) * x0))%expr) + Datatypes.Some + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (- ($(v (Compile.reflect x1)) * $x0)); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end @@ -725,9 +851,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv <- ident.unify pattern.ident.Literal ##(projT2 args); xv0 <- ident.unify pattern.ident.Literal ##(projT2 args0); Datatypes.Some - (Base - (##((let (x1, _) := xv in x1) * - (let (x1, _) := xv0 in x1))%Z)%expr) + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ##((let (x1, _) := xv in x1) * + (let (x1, _) := xv0 in x1)); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end @@ -744,7 +872,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ℤ -> s)%ptype then v <- type.try_make_transport_cps s ℤ; - Datatypes.Some (Base (- (x * v (Compile.reflect x1)))%expr) + Datatypes.Some + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (- ($x * $(v (Compile.reflect x1)))); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end @@ -769,8 +901,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if (let (x1, _) := xv in x1) <? 0 then Datatypes.Some - (Base - (- (##(- (let (x1, _) := xv in x1))%Z * x0))%expr) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (- (##(- (let (x1, _) := xv in x1))%Z * $x0))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -795,8 +928,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if (let (x1, _) := xv in x1) <? 0 then Datatypes.Some - (Base - (- (x * ##(- (let (x1, _) := xv in x1))%Z))%expr) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (- ($x * ##(- (let (x1, _) := xv in x1))%Z))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -820,8 +954,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with negb ((let (x1, _) := xv in x1) =? 2) then Datatypes.Some - (Base - (x << ##(Z.log2 (let (x1, _) := xv in x1)))%expr) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x << ##(Z.log2 (let (x1, _) := xv in x1)))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -849,8 +984,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with negb ((let (x1, _) := xv in x1) =? 2) then Datatypes.Some - (Base - (x0 << ##(Z.log2 (let (x1, _) := xv in x1)))%expr) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x0 << ##(Z.log2 (let (x1, _) := xv in x1)))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -894,11 +1030,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with Z.abs max_const_val) then Datatypes.Some - (Base - (v (Compile.reflect x4) * - (v0 (Compile.reflect x3) * + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false + ($(v (Compile.reflect x4)) * + ($(v0 (Compile.reflect x3)) * (##(let (x5, _) := xv in x5) * - ##(let (x5, _) := xv0 in x5))))%expr) + ##(let (x5, _) := xv0 in x5))))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -951,11 +1089,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with Z.abs max_const_val) then Datatypes.Some - (Base - (v (Compile.reflect x2) * - (v0 (Compile.reflect x4) * + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($(v (Compile.reflect x2)) * + ($(v0 (Compile.reflect x4)) * (##(let (x5, _) := xv in x5) * - ##(let (x5, _) := xv0 in x5))))%expr) + ##(let (x5, _) := xv0 in x5))))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -996,10 +1135,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with Z.abs max_const_val then Datatypes.Some - (Base - (v (Compile.reflect x2) * - (v0 (Compile.reflect x1) * - ##(let (x3, _) := xv in x3)))%expr) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($(v (Compile.reflect x2)) * + ($(v0 (Compile.reflect x1)) * + ##(let (x3, _) := xv in x3)))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1034,7 +1174,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with Z.abs max_const_val then Datatypes.Some - (Base (x0 * ##(let (x1, _) := xv in x1))%expr) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x0 * ##(let (x1, _) := xv in x1))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1067,7 +1209,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s ℤ; fv <- (if (let (x2, _) := xv in x2) =? 0 then - Datatypes.Some (Base (v (Compile.reflect x1))) + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($(v (Compile.reflect x1)))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1092,7 +1237,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (if (let (x1, _) := xv in x1) =? 0 - then Datatypes.Some (Base (- x0)%expr) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (- $x0)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1115,7 +1264,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (if (let (x1, _) := xv in x1) =? 0 - then Datatypes.Some (Base x) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1138,8 +1291,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s0 ℤ; v0 <- type.try_make_transport_cps s ℤ; Datatypes.Some - (Base - (v0 (Compile.reflect x1) - v (Compile.reflect x2))%expr) + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($(v0 (Compile.reflect x1)) - + $(v (Compile.reflect x2))); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end @@ -1166,7 +1322,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (s -> ℤ)%ptype then v <- type.try_make_transport_cps s ℤ; - Datatypes.Some (Base (- (v (Compile.reflect x1) + x0))%expr) + Datatypes.Some + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (- ($(v (Compile.reflect x1)) + $x0)); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end @@ -1187,7 +1347,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ℤ -> s)%ptype then v <- type.try_make_transport_cps s ℤ; - Datatypes.Some (Base (x + v (Compile.reflect x1))%expr) + Datatypes.Some + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x + $(v (Compile.reflect x1))); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end);; @@ -1209,9 +1373,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if (let (x2, _) := xv in x2) >? 0 then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false (##(let (x2, _) := xv in x2) + - v (Compile.reflect x1))%expr) + $(v (Compile.reflect x1)))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1234,9 +1399,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if (let (x2, _) := xv in x2) <? 0 then Datatypes.Some - (Base - (v (Compile.reflect x1) - - ##(- (let (x2, _) := xv in x2))%Z)%expr) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($(v (Compile.reflect x1)) - + ##(- (let (x2, _) := xv in x2))%Z)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1266,8 +1432,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if (let (x1, _) := xv in x1) <? 0 then Datatypes.Some - (Base - (- (##(- (let (x1, _) := xv in x1))%Z + x0))%expr) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (- (##(- (let (x1, _) := xv in x1))%Z + $x0))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1293,10 +1460,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if (let (x2, _) := xv in x2) >? 0 then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false (- - (v (Compile.reflect x1) + - ##(let (x2, _) := xv in x2)))%expr) + ($(v (Compile.reflect x1)) + + ##(let (x2, _) := xv in x2)))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1319,9 +1487,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if (let (x2, _) := xv in x2) <? 0 then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false (##(- (let (x2, _) := xv in x2))%Z - - v (Compile.reflect x1))%expr) + $(v (Compile.reflect x1)))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1351,7 +1520,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if (let (x1, _) := xv in x1) <? 0 then Datatypes.Some - (Base (x + ##(- (let (x1, _) := xv in x1))%Z)%expr) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x + ##(- (let (x1, _) := xv in x1))%Z)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1364,38 +1535,41 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with Base (x - x0)%expr)%option | Z_opp => fun x : expr ℤ => - (((match x with - | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x0 => - _ <- invert_bind_args idc Raw.ident.Z_opp; - match pattern.type.unify_extracted ℤ s with - | Datatypes.Some _ => - if type.type_beq base.type base.type.type_beq ℤ s - then - v <- type.try_make_transport_cps s ℤ; - Datatypes.Some (Base (v (Compile.reflect x0))) - else Datatypes.None - | Datatypes.None => Datatypes.None - end - | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ - (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | - @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None - | _ => Datatypes.None - end;; - match pattern.type.unify_extracted ℤ ℤ with - | Datatypes.Some _ => - if type.type_beq base.type base.type.type_beq ℤ ℤ - then - fv <- (if negb (SubstVarLike.is_var_fst_snd_pair_opp_cast x) - then - Datatypes.Some - (UnderLet x (fun v : var ℤ => Base (- $v)%expr)) - else Datatypes.None); - Datatypes.Some (fv0 <-- fv; - Base fv0)%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end);; - Datatypes.None);;; + ((match x with + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x0 => + _ <- invert_bind_args idc Raw.ident.Z_opp; + match pattern.type.unify_extracted ℤ s with + | Datatypes.Some _ => + if type.type_beq base.type base.type.type_beq ℤ s + then + v <- type.try_make_transport_cps s ℤ; + Datatypes.Some + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($(v (Compile.reflect x0))); + Base fv)%under_lets + else Datatypes.None + | Datatypes.None => Datatypes.None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | + @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None + | _ => Datatypes.None + end;; + match pattern.type.unify_extracted ℤ ℤ with + | Datatypes.Some _ => + if type.type_beq base.type base.type.type_beq ℤ ℤ + then + fv <- (if negb (SubstVarLike.is_var_fst_snd_pair_opp_cast x) + then + Datatypes.Some + (UnderLet x (fun v : var ℤ => Base (- $v)%expr)) + else Datatypes.None); + Datatypes.Some (fv0 <-- fv; + Base fv0)%under_lets + else Datatypes.None + | Datatypes.None => Datatypes.None + end);;; Base (- x)%expr)%option | Z_div => fun x x0 : expr ℤ => @@ -1413,7 +1587,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (if (let (x1, _) := xv in x1) =? 1 - then Datatypes.Some (Base x) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1436,8 +1614,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 2 ^ Z.log2 (let (x1, _) := xv in x1) then Datatypes.Some - (Base - (x >> ##(Z.log2 (let (x1, _) := xv in x1)))%expr) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x >> ##(Z.log2 (let (x1, _) := xv in x1)))) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1464,7 +1643,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (if (let (x1, _) := xv in x1) =? 1 - then Datatypes.Some (Base (##0)%expr) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false ##0) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1487,7 +1669,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 2 ^ Z.log2 (let (x1, _) := xv in x1) then Datatypes.Some - (Base (x &' ##((let (x1, _) := xv in x1) - 1)%Z)%expr) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x &' ##((let (x1, _) := xv in x1) - 1)%Z)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1524,7 +1708,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then xv <- ident.unify pattern.ident.Literal ##(projT2 args); fv <- (if (let (x1, _) := xv in x1) =? 0 - then Datatypes.Some (Base (##0)%expr) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false ##0) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1545,13 +1732,229 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fun x x0 x1 : expr ℤ => Base (#(Z_mul_split)%expr @ x @ x0 @ x1)%expr_pat | Z_add_get_carry => fun x x0 x1 : expr ℤ => - Base (#(Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat + ((match x1 with + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x2 => + _ <- invert_bind_args idc Raw.ident.Z_opp; + match + pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype + ((ℤ -> ℤ) -> s)%ptype + with + | Datatypes.Some (_, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> ℤ) -> s)%ptype + then + v <- type.try_make_transport_cps s ℤ; + Datatypes.Some + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v0 := (#(Z_sub_get_borrow)%expr @ + ($x)%expr @ ($x0)%expr @ + ($(v (Compile.reflect x2)))%expr)%expr_pat in + (#(fst)%expr @ $v0, + - (#(snd)%expr @ $v0)%expr_pat)%expr_pat); + Base fv)%under_lets + else Datatypes.None + | Datatypes.None => Datatypes.None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | + @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None + | _ => Datatypes.None + end;; + match x0 with + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x2 => + _ <- invert_bind_args idc Raw.ident.Z_opp; + match + pattern.type.unify_extracted ((ℤ -> ℤ) -> ℤ)%ptype + ((ℤ -> s) -> ℤ)%ptype + with + | Datatypes.Some (_, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + ((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> s) -> ℤ)%ptype + then + v <- type.try_make_transport_cps s ℤ; + Datatypes.Some + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v0 := (#(Z_sub_get_borrow)%expr @ + ($x)%expr @ ($x1)%expr @ + ($(v (Compile.reflect x2)))%expr)%expr_pat in + (#(fst)%expr @ $v0, + - (#(snd)%expr @ $v0)%expr_pat)%expr_pat); + Base fv)%under_lets + else Datatypes.None + | Datatypes.None => Datatypes.None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | + @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None + | _ => Datatypes.None + end);;; + Base (#(Z_add_get_carry)%expr @ x @ x0 @ x1)%expr_pat)%option | Z_add_with_carry => fun x x0 x1 : expr ℤ => Base (#(Z_add_with_carry)%expr @ x @ x0 @ x1)%expr_pat | Z_add_with_get_carry => fun x x0 x1 x2 : expr ℤ => - Base (#(Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat + (match x0 with + | @expr.Ident _ _ _ t idc => + match x2 with + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t0 idc0) x3 => + _ <- invert_bind_args idc0 Raw.ident.Z_opp; + args0 <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((ℤ -> (projT1 args0)) -> ℤ) -> s)%ptype + with + | Datatypes.Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((ℤ -> (projT1 args0)) -> ℤ) -> s)%ptype + then + xv <- ident.unify pattern.ident.Literal ##(projT2 args0); + v <- type.try_make_transport_cps s ℤ; + fv <- (if (let (x4, _) := xv in x4) =? 0 + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v0 := (#(Z_sub_get_borrow)%expr @ + ($x)%expr @ ($x1)%expr @ + ($(v (Compile.reflect x3)))%expr)%expr_pat in + (#(fst)%expr @ $v0, + - (#(snd)%expr @ $v0)%expr_pat)%expr_pat)) + else Datatypes.None); + Datatypes.Some (fv0 <-- fv; + Base fv0)%under_lets + else Datatypes.None + | Datatypes.None => Datatypes.None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat + _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => + Datatypes.None + | _ => Datatypes.None + end;; + match x1 with + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t0 idc0) x3 => + _ <- invert_bind_args idc0 Raw.ident.Z_opp; + args0 <- invert_bind_args idc Raw.ident.Literal; + match + pattern.type.unify_extracted (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((ℤ -> (projT1 args0)) -> s) -> ℤ)%ptype + with + | Datatypes.Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((ℤ -> (projT1 args0)) -> s) -> ℤ)%ptype + then + xv <- ident.unify pattern.ident.Literal ##(projT2 args0); + v <- type.try_make_transport_cps s ℤ; + fv <- (if (let (x4, _) := xv in x4) =? 0 + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v0 := (#(Z_sub_get_borrow)%expr @ + ($x)%expr @ ($x2)%expr @ + ($(v (Compile.reflect x3)))%expr)%expr_pat in + (#(fst)%expr @ $v0, + - (#(snd)%expr @ $v0)%expr_pat)%expr_pat)) + else Datatypes.None); + Datatypes.Some (fv0 <-- fv; + Base fv0)%under_lets + else Datatypes.None + | Datatypes.None => Datatypes.None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat + _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => + Datatypes.None + | _ => Datatypes.None + end + | @expr.App _ _ _ s _ (@expr.Ident _ _ _ t idc) x3 => + match x1 with + | @expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x4 => + _ <- invert_bind_args idc0 Raw.ident.Z_opp; + _ <- invert_bind_args idc Raw.ident.Z_opp; + match + pattern.type.unify_extracted (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((ℤ -> s) -> s0) -> ℤ)%ptype + with + | Datatypes.Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((ℤ -> s) -> s0) -> ℤ)%ptype + then + v <- type.try_make_transport_cps s ℤ; + v0 <- type.try_make_transport_cps s0 ℤ; + Datatypes.Some + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v1 := (#(Z_sub_with_get_borrow)%expr @ + ($x)%expr @ + ($(v (Compile.reflect x3)))%expr @ + ($x2)%expr @ + ($(v0 (Compile.reflect x4)))%expr)%expr_pat in + (#(fst)%expr @ $v1, + - (#(snd)%expr @ $v1)%expr_pat)%expr_pat); + Base fv)%under_lets + else Datatypes.None + | Datatypes.None => Datatypes.None + end + | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _ (_ @ _)%expr_pat + _ | @expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _ => + Datatypes.None + | _ => Datatypes.None + end;; + match x2 with + | @expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x4 => + _ <- invert_bind_args idc0 Raw.ident.Z_opp; + _ <- invert_bind_args idc Raw.ident.Z_opp; + match + pattern.type.unify_extracted (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((ℤ -> s) -> ℤ) -> s0)%ptype + with + | Datatypes.Some (_, _, _, _)%zrange => + if + type.type_beq base.type base.type.type_beq + (((ℤ -> ℤ) -> ℤ) -> ℤ)%ptype + (((ℤ -> s) -> ℤ) -> s0)%ptype + then + v <- type.try_make_transport_cps s ℤ; + v0 <- type.try_make_transport_cps s0 ℤ; + Datatypes.Some + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v1 := (#(Z_sub_with_get_borrow)%expr @ + ($x)%expr @ + ($(v (Compile.reflect x3)))%expr @ + ($x1)%expr @ + ($(v0 (Compile.reflect x4)))%expr)%expr_pat in + (#(fst)%expr @ $v1, + - (#(snd)%expr @ $v1)%expr_pat)%expr_pat); + Base fv)%under_lets + else Datatypes.None + | Datatypes.None => Datatypes.None + end + | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _ (_ @ _)%expr_pat + _ | @expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _ => + Datatypes.None + | _ => Datatypes.None + end + | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | + @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => Datatypes.None + | _ => Datatypes.None + end;;; + Base (#(Z_add_with_get_carry)%expr @ x @ x0 @ x1 @ x2)%expr_pat)%option | Z_sub_get_borrow => fun x x0 x1 : expr ℤ => Base (#(Z_sub_get_borrow)%expr @ x @ x0 @ x1)%expr_pat @@ -1567,54 +1970,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fun x x0 x1 x2 : expr ℤ => Base (#(Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat | Z_cc_m => fun x x0 : expr ℤ => Base (#(Z_cc_m)%expr @ x @ x0)%expr_pat +| Z_combine_at_bitwidth => + fun x x0 x1 : expr ℤ => + Base (#(Z_combine_at_bitwidth)%expr @ x @ x0 @ x1)%expr_pat | Z_cast range => fun x : expr ℤ => Base (#(Z_cast range)%expr @ x)%expr_pat | Z_cast2 range => - fun x : expr (ℤ * ℤ)%etype => - (match x with - | @expr.App _ _ _ s _ - (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x1) x0 => - args <- invert_bind_args idc Raw.ident.pair; - match - pattern.type.unify_extracted - (((ℤ -> ℤ -> (ℤ * ℤ)%pbtype) -> ℤ) -> ℤ)%ptype - ((((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 (_, (_, (_, _)), _, _)%zrange => - if - type.type_beq base.type base.type.type_beq - (((ℤ -> ℤ -> (ℤ * ℤ)%etype) -> ℤ) -> ℤ)%ptype - ((((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.pair pair; - v <- type.try_make_transport_cps s0 ℤ; - v0 <- type.try_make_transport_cps s ℤ; - Datatypes.Some - (fv0 <-- do_again (ℤ * ℤ) - (#(Z_cast (Datatypes.fst range))%expr @ - ($(v (Compile.reflect x1)))%expr, - #(Z_cast (Datatypes.snd range))%expr @ - ($(v0 (Compile.reflect x0)))%expr)%expr_pat; - Base fv0)%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;;; - Base (#(Z_cast2 range)%expr @ x)%expr_pat)%option + 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 => diff --git a/src/arith_with_casts_rewrite_head.out b/src/arith_with_casts_rewrite_head.out index 06e7a732b..6eb141dfc 100644 --- a/src/arith_with_casts_rewrite_head.out +++ b/src/arith_with_casts_rewrite_head.out @@ -47,7 +47,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with _ <- 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 (Base (v4 (v3 (v1 (v (Compile.reflect x1)))))) + 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 @@ -100,7 +104,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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 (Base (v4 (v3 (v2 (v0 (Compile.reflect x0)))))) + 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 @@ -151,6 +159,26 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with to_expr (x0 ($x3) (fun x6 : expr P => Base ($x4 @ x6)%expr_pat) ($x5)))%expr @ x1 @ x2)%expr_pat +| @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)) @@ -160,6 +188,43 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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 +| @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 + (#(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 +| @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)) @@ -218,6 +283,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | @List_nth_default T => fun (x : expr T) (x0 : expr (list T)) (x1 : expr ℕ) => Base (#(List_nth_default)%expr @ x @ x0 @ x1)%expr_pat +| @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 @@ -237,7 +305,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if is_bounded_by_bool 0 (ZRange.normalize args0) && ((let (x2, _) := xv in x2) =? 0) - then Datatypes.Some (Base x0) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x0)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -268,7 +340,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if is_bounded_by_bool 0 (ZRange.normalize args0) && ((let (x2, _) := xv in x2) =? 0) - then Datatypes.Some (Base x) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -305,7 +381,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if is_bounded_by_bool 0 (ZRange.normalize args0) && ((let (x2, _) := xv in x2) =? 0) - then Datatypes.Some (Base (- x0)%expr) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (- $x0)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -339,8 +419,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x5, _) := xv in x5) =? 0) then Datatypes.Some - (Base - (#(Z_cast args)%expr @ v (Compile.reflect x4))%expr_pat) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (#(Z_cast args)%expr @ + ($(v (Compile.reflect x4)))%expr)%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -403,8 +485,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ZRange.normalize args <=? - ZRange.normalize args1)%zrange then Datatypes.Some - (Base - (#(Z_cast args)%expr @ v (Compile.reflect x2))%expr_pat) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (#(Z_cast args)%expr @ + ($(v (Compile.reflect x2)))%expr)%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -472,7 +556,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if is_bounded_by_bool 0 (ZRange.normalize args0) && ((let (x2, _) := xv in x2) =? 0) - then Datatypes.Some (Base (##0)%expr) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false ##0) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -515,7 +602,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x3, _) := xv in x3) =? 0) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false (#(Z_cast r[0 ~> 0])%expr @ (##0)%expr, #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat) else Datatypes.None); @@ -552,7 +640,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x3, _) := xv in x3) =? 0) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false (#(Z_cast r[0 ~> 0])%expr @ (##0)%expr, #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat) else Datatypes.None); @@ -600,9 +689,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x5, _) := xv0 in x5) =? 1) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast args3)%expr @ - v (Compile.reflect x2), + ($(v (Compile.reflect x2)))%expr, #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat) else Datatypes.None); @@ -646,9 +737,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x5, _) := xv0 in x5) =? 1) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast args0)%expr @ - v (Compile.reflect x4), + ($(v (Compile.reflect x4)))%expr, #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat) else Datatypes.None); @@ -728,7 +821,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ZRange.normalize args0) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false ((##(Datatypes.fst (Z.add_get_carry_full (let (x5, _) := xv in @@ -784,9 +879,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x5, _) := xv0 in x5) =? 0) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast args)%expr @ - v (Compile.reflect x4), + ($(v (Compile.reflect x4)))%expr, #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -833,9 +930,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x5, _) := xv0 in x5) =? 0) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false (#(Z_cast args1)%expr @ - v (Compile.reflect x3), + ($(v (Compile.reflect x3)))%expr, #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -884,7 +982,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if is_bounded_by_bool 0 (ZRange.normalize args0) && ((let (x3, _) := xv in x3) =? 0) - then Datatypes.Some (Base (x0 + x1)%expr) + then + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ($x0 + $x1)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -957,7 +1059,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ZRange.normalize args0) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota + var) false ((##(Datatypes.fst (Z.add_with_get_carry_full (let (x7, _) := @@ -1035,9 +1139,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x7, _) := xv1 in x7) =? 0) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast args)%expr @ - v (Compile.reflect x6), + ($(v (Compile.reflect x6)))%expr, #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat) else Datatypes.None); @@ -1097,9 +1203,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x7, _) := xv1 in x7) =? 0) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast args1)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, #(Z_cast r[0 ~> 0])%expr @ (##0)%expr)%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -1150,6 +1258,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fun x x0 x1 x2 : expr ℤ => Base (#(Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat | Z_cc_m => fun x x0 : expr ℤ => Base (#(Z_cc_m)%expr @ x @ x0)%expr_pat +| Z_combine_at_bitwidth => + fun x x0 x1 : expr ℤ => + Base (#(Z_combine_at_bitwidth)%expr @ x @ x0 @ x1)%expr_pat | Z_cast range => fun x : expr ℤ => (((match pattern.type.unify_extracted ℤ ℤ with @@ -1159,7 +1270,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv <- (if lower range =? upper range then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false (#(Z_cast range)%expr @ (##(lower range))%expr)%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -1179,8 +1291,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ZRange.normalize args <=? ZRange.normalize range)%zrange then Datatypes.Some - (Base - (#(Z_cast args)%expr @ v (Compile.reflect x0))%expr_pat) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (#(Z_cast args)%expr @ + ($(v (Compile.reflect x0)))%expr)%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1204,12 +1318,15 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s0 ℤ; v1 <- type.try_make_transport_cps s ℤ; Datatypes.Some - (UnderLet - (#(Z_cast range)%expr @ - (#(Z_add_with_carry)%expr @ v (Compile.reflect x2) @ - v0 (Compile.reflect x1) @ v1 (Compile.reflect x0)))%expr_pat - (fun v2 : var ℤ => - Base (#(Z_cast range)%expr @ ($v2)%expr)%expr_pat)) + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v2 := (#(Z_cast range)%expr @ + (#(Z_add_with_carry)%expr @ + ($(v (Compile.reflect x2)))%expr @ + ($(v0 (Compile.reflect x1)))%expr @ + ($(v1 (Compile.reflect x0)))%expr))%expr_pat in + (#(Z_cast range)%expr @ $v2)%expr_pat); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end @@ -1264,12 +1381,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- type.try_make_transport_cps s0 ℤ; v0 <- type.try_make_transport_cps s ℤ; Datatypes.Some - (fv0 <-- do_again (ℤ * ℤ) + (fv0 <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) true (#(Z_cast (Datatypes.fst range))%expr @ ($(v (Compile.reflect x1)))%expr, #(Z_cast (Datatypes.snd range))%expr @ ($(v0 (Compile.reflect x0)))%expr)%expr_pat; - Base fv0)%under_lets + fv1 <-- do_again (ℤ * ℤ) fv0; + Base fv1)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end @@ -1301,30 +1420,28 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with - ZRange.normalize args1)%zrange then Datatypes.Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_get_borrow)%expr @ - v (Compile.reflect x2) @ - v1 (Compile.reflect x0) @ - (#(Z_cast args)%expr @ - v0 (Compile.reflect x5))))%expr_pat - (fun v2 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($v2)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ $v2)))%expr_pat)%expr)%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v2 := (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_get_borrow)%expr @ + ($(v (Compile.reflect x2)))%expr @ + ($(v1 (Compile.reflect x0)))%expr @ + (#(Z_cast args)%expr @ + ($(v0 (Compile.reflect x5)))%expr)))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ $v2)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ $v2)))%expr_pat))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1385,30 +1502,28 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with - ZRange.normalize args1)%zrange then Datatypes.Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_get_borrow)%expr @ - v (Compile.reflect x2) @ - v0 (Compile.reflect x1) @ - (#(Z_cast args)%expr @ - v1 (Compile.reflect x5))))%expr_pat - (fun v2 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($v2)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ $v2)))%expr_pat)%expr)%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v2 := (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_get_borrow)%expr @ + ($(v (Compile.reflect x2)))%expr @ + ($(v0 (Compile.reflect x1)))%expr @ + (#(Z_cast args)%expr @ + ($(v1 (Compile.reflect x5)))%expr)))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ $v2)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ $v2)))%expr_pat))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1467,30 +1582,30 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x4, _) := xv in x4) <? 0) then Datatypes.Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_get_borrow)%expr @ - v (Compile.reflect x2) @ - v0 (Compile.reflect x0) @ - (#(Z_cast (- args0))%expr @ - (##(- (let (x4, _) := xv in x4))%Z)%expr)))%expr_pat - (fun v1 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($v1)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ $v1)))%expr_pat)%expr)%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v1 := (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_get_borrow)%expr @ + ($(v (Compile.reflect x2)))%expr @ + ($(v0 (Compile.reflect x0)))%expr @ + (#(Z_cast (- args0))%expr @ + (##(- + (let (x4, _) := xv in + x4))%Z)%expr)))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ $v1)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ $v1)))%expr_pat))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1528,30 +1643,30 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x4, _) := xv in x4) <? 0) then Datatypes.Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_get_borrow)%expr @ - v (Compile.reflect x2) @ - v0 (Compile.reflect x1) @ - (#(Z_cast (- args0))%expr @ - (##(- (let (x4, _) := xv in x4))%Z)%expr)))%expr_pat - (fun v1 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($v1)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ $v1)))%expr_pat)%expr)%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v1 := (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + (#(Z_sub_get_borrow)%expr @ + ($(v (Compile.reflect x2)))%expr @ + ($(v0 (Compile.reflect x1)))%expr @ + (#(Z_cast (- args0))%expr @ + (##(- + (let (x4, _) := xv in + x4))%Z)%expr)))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ $v1)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ $v1)))%expr_pat))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1579,16 +1694,18 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s0 ℤ; v1 <- type.try_make_transport_cps s ℤ; Datatypes.Some - (UnderLet - (#(Z_cast2 range)%expr @ - (#(Z_add_get_carry)%expr @ v (Compile.reflect x2) @ - v0 (Compile.reflect x1) @ v1 (Compile.reflect x0)))%expr_pat - (fun v2 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ (#(Z_cast2 range)%expr @ ($v2)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (#(snd)%expr @ (#(Z_cast2 range)%expr @ ($v2)%expr)))%expr_pat)) + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v2 := (#(Z_cast2 range)%expr @ + (#(Z_add_get_carry)%expr @ + ($(v (Compile.reflect x2)))%expr @ + ($(v0 (Compile.reflect x1)))%expr @ + ($(v1 (Compile.reflect x0)))%expr))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ (#(Z_cast2 range)%expr @ $v2)), + #(Z_cast (Datatypes.snd range))%expr @ + (#(snd)%expr @ (#(Z_cast2 range)%expr @ $v2)))%expr_pat); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end);; @@ -1606,16 +1723,18 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s0 ℤ; v1 <- type.try_make_transport_cps s ℤ; Datatypes.Some - (UnderLet - (#(Z_cast2 range)%expr @ - (#(Z_sub_get_borrow)%expr @ v (Compile.reflect x2) @ - v0 (Compile.reflect x1) @ v1 (Compile.reflect x0)))%expr_pat - (fun v2 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ (#(Z_cast2 range)%expr @ ($v2)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (#(snd)%expr @ (#(Z_cast2 range)%expr @ ($v2)%expr)))%expr_pat)) + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v2 := (#(Z_cast2 range)%expr @ + (#(Z_sub_get_borrow)%expr @ + ($(v (Compile.reflect x2)))%expr @ + ($(v0 (Compile.reflect x1)))%expr @ + ($(v1 (Compile.reflect x0)))%expr))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ (#(Z_cast2 range)%expr @ $v2)), + #(Z_cast (Datatypes.snd range))%expr @ + (#(snd)%expr @ (#(Z_cast2 range)%expr @ $v2)))%expr_pat); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end);; @@ -1633,16 +1752,18 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s0 ℤ; v1 <- type.try_make_transport_cps s ℤ; Datatypes.Some - (UnderLet - (#(Z_cast2 range)%expr @ - (#(Z_mul_split)%expr @ v (Compile.reflect x2) @ - v0 (Compile.reflect x1) @ v1 (Compile.reflect x0)))%expr_pat - (fun v2 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ (#(Z_cast2 range)%expr @ ($v2)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (#(snd)%expr @ (#(Z_cast2 range)%expr @ ($v2)%expr)))%expr_pat)) + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v2 := (#(Z_cast2 range)%expr @ + (#(Z_mul_split)%expr @ + ($(v (Compile.reflect x2)))%expr @ + ($(v0 (Compile.reflect x1)))%expr @ + ($(v1 (Compile.reflect x0)))%expr))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ (#(Z_cast2 range)%expr @ $v2)), + #(Z_cast (Datatypes.snd range))%expr @ + (#(snd)%expr @ (#(Z_cast2 range)%expr @ $v2)))%expr_pat); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end @@ -1689,32 +1810,40 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x8, _) := xv in x8) =? 0) then Datatypes.Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_get_borrow)%expr @ - v (Compile.reflect x3) @ - v1 (Compile.reflect x0) @ - (#(Z_cast args)%expr @ - v0 (Compile.reflect x7))))%expr_pat - (fun v2 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($v2)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast - (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $v2)))%expr_pat)%expr)%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false + (expr_let v2 := (#(Z_cast2 + (Datatypes.fst + range, + - + Datatypes.snd + range))%expr @ + (#(Z_sub_get_borrow)%expr @ + ($(v + (Compile.reflect + x3)))%expr @ + ($(v1 + (Compile.reflect + x0)))%expr @ + (#(Z_cast args)%expr @ + ($(v0 + (Compile.reflect + x7)))%expr)))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v2)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v2)))%expr_pat))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1753,33 +1882,46 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with - ZRange.normalize args1)%zrange then Datatypes.Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ - v (Compile.reflect x3) @ - (#(Z_cast (- args3))%expr @ - (##(- (let (x8, _) := xv in x8))%Z)%expr) @ - v1 (Compile.reflect x0) @ - (#(Z_cast args)%expr @ - v0 (Compile.reflect x7))))%expr_pat - (fun v2 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($v2)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $v2)))%expr_pat)%expr)%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false + (expr_let v2 := (#(Z_cast2 + (Datatypes.fst + range, + - + Datatypes.snd + range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + ($(v + (Compile.reflect + x3)))%expr @ + (#(Z_cast (- args3))%expr @ + (##(- + (let + (x8, _) := + xv in + x8))%Z)%expr) @ + ($(v1 + (Compile.reflect + x0)))%expr @ + (#(Z_cast args)%expr @ + ($(v0 + (Compile.reflect + x7)))%expr)))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v2)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v2)))%expr_pat))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1855,32 +1997,40 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x8, _) := xv in x8) =? 0) then Datatypes.Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_get_borrow)%expr @ - v (Compile.reflect x3) @ - v0 (Compile.reflect x1) @ - (#(Z_cast args)%expr @ - v1 (Compile.reflect x7))))%expr_pat - (fun v2 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($v2)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast - (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $v2)))%expr_pat)%expr)%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false + (expr_let v2 := (#(Z_cast2 + (Datatypes.fst + range, + - + Datatypes.snd + range))%expr @ + (#(Z_sub_get_borrow)%expr @ + ($(v + (Compile.reflect + x3)))%expr @ + ($(v0 + (Compile.reflect + x1)))%expr @ + (#(Z_cast args)%expr @ + ($(v1 + (Compile.reflect + x7)))%expr)))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v2)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v2)))%expr_pat))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -1919,33 +2069,46 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with - ZRange.normalize args1)%zrange then Datatypes.Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ - v (Compile.reflect x3) @ - (#(Z_cast (- args3))%expr @ - (##(- (let (x8, _) := xv in x8))%Z)%expr) @ - v0 (Compile.reflect x1) @ - (#(Z_cast args)%expr @ - v1 (Compile.reflect x7))))%expr_pat - (fun v2 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($v2)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $v2)))%expr_pat)%expr)%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false + (expr_let v2 := (#(Z_cast2 + (Datatypes.fst + range, + - + Datatypes.snd + range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + ($(v + (Compile.reflect + x3)))%expr @ + (#(Z_cast (- args3))%expr @ + (##(- + (let + (x8, _) := + xv in + x8))%Z)%expr) @ + ($(v0 + (Compile.reflect + x1)))%expr @ + (#(Z_cast args)%expr @ + ($(v1 + (Compile.reflect + x7)))%expr)))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v2)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v2)))%expr_pat))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2024,33 +2187,48 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ZRange.normalize args2) then Datatypes.Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ - v (Compile.reflect x3) @ - (#(Z_cast (- args2))%expr @ - (##(- (let (x6, _) := xv in x6))%Z)%expr) @ - v0 (Compile.reflect x0) @ - (#(Z_cast (- args0))%expr @ - (##(- (let (x6, _) := xv0 in x6))%Z)%expr)))%expr_pat - (fun v1 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($v1)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $v1)))%expr_pat)%expr)%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false + (expr_let v1 := (#(Z_cast2 + (Datatypes.fst + range, + - + Datatypes.snd + range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + ($(v + (Compile.reflect + x3)))%expr @ + (#(Z_cast (- args2))%expr @ + (##(- + (let + (x6, _) := + xv in + x6))%Z)%expr) @ + ($(v0 + (Compile.reflect + x0)))%expr @ + (#(Z_cast (- args0))%expr @ + (##(- + (let + (x6, _) := + xv0 in + x6))%Z)%expr)))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v1)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v1)))%expr_pat))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2102,33 +2280,48 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ZRange.normalize args2) then Datatypes.Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ - v (Compile.reflect x3) @ - (#(Z_cast (- args2))%expr @ - (##(- (let (x6, _) := xv in x6))%Z)%expr) @ - v0 (Compile.reflect x1) @ - (#(Z_cast (- args0))%expr @ - (##(- (let (x6, _) := xv0 in x6))%Z)%expr)))%expr_pat - (fun v1 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($v1)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $v1)))%expr_pat)%expr)%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false + (expr_let v1 := (#(Z_cast2 + (Datatypes.fst + range, + - + Datatypes.snd + range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + ($(v + (Compile.reflect + x3)))%expr @ + (#(Z_cast (- args2))%expr @ + (##(- + (let + (x6, _) := + xv in + x6))%Z)%expr) @ + ($(v0 + (Compile.reflect + x1)))%expr @ + (#(Z_cast (- args0))%expr @ + (##(- + (let + (x6, _) := + xv0 in + x6))%Z)%expr)))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v1)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v1)))%expr_pat))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2165,20 +2358,25 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x5, _) := xv in x5) =? 0) then Datatypes.Some - (UnderLet - (#(Z_cast2 range)%expr @ - (#(Z_add_get_carry)%expr @ - v (Compile.reflect x3) @ - v0 (Compile.reflect x1) @ - v1 (Compile.reflect x0)))%expr_pat - (fun v2 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 range)%expr @ ($v2)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 range)%expr @ ($v2)%expr)))%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v2 := (#(Z_cast2 range)%expr @ + (#(Z_add_get_carry)%expr @ + ($(v + (Compile.reflect + x3)))%expr @ + ($(v0 + (Compile.reflect + x1)))%expr @ + ($(v1 + (Compile.reflect + x0)))%expr))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 range)%expr @ $v2)), + #(Z_cast (Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 range)%expr @ $v2)))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2221,33 +2419,44 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with - ZRange.normalize args4)%zrange then Datatypes.Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ - v (Compile.reflect x3) @ - (#(Z_cast args2)%expr @ - v0 (Compile.reflect x6)) @ - v2 (Compile.reflect x0) @ - (#(Z_cast args)%expr @ - v1 (Compile.reflect x9))))%expr_pat - (fun v3 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($v3)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $v3)))%expr_pat)%expr)%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false + (expr_let v3 := (#(Z_cast2 + (Datatypes.fst + range, + - + Datatypes.snd + range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + ($(v + (Compile.reflect + x3)))%expr @ + (#(Z_cast args2)%expr @ + ($(v0 + (Compile.reflect + x6)))%expr) @ + ($(v2 + (Compile.reflect + x0)))%expr @ + (#(Z_cast args)%expr @ + ($(v1 + (Compile.reflect + x9)))%expr)))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v3)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v3)))%expr_pat))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2322,33 +2531,44 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with - ZRange.normalize args4)%zrange then Datatypes.Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ - v (Compile.reflect x3) @ - (#(Z_cast args2)%expr @ - v0 (Compile.reflect x6)) @ - v1 (Compile.reflect x1) @ - (#(Z_cast args)%expr @ - v2 (Compile.reflect x9))))%expr_pat - (fun v3 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($v3)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $v3)))%expr_pat)%expr)%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false + (expr_let v3 := (#(Z_cast2 + (Datatypes.fst + range, + - + Datatypes.snd + range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + ($(v + (Compile.reflect + x3)))%expr @ + (#(Z_cast args2)%expr @ + ($(v0 + (Compile.reflect + x6)))%expr) @ + ($(v1 + (Compile.reflect + x1)))%expr @ + (#(Z_cast args)%expr @ + ($(v2 + (Compile.reflect + x9)))%expr)))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v3)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v3)))%expr_pat))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2423,33 +2643,46 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with - ZRange.normalize args3)%zrange then Datatypes.Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ - v (Compile.reflect x3) @ - (#(Z_cast args1)%expr @ - v0 (Compile.reflect x6)) @ - v1 (Compile.reflect x0) @ - (#(Z_cast (- args0))%expr @ - (##(- (let (x8, _) := xv in x8))%Z)%expr)))%expr_pat - (fun v2 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($v2)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $v2)))%expr_pat)%expr)%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false + (expr_let v2 := (#(Z_cast2 + (Datatypes.fst + range, + - + Datatypes.snd + range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + ($(v + (Compile.reflect + x3)))%expr @ + (#(Z_cast args1)%expr @ + ($(v0 + (Compile.reflect + x6)))%expr) @ + ($(v1 + (Compile.reflect + x0)))%expr @ + (#(Z_cast (- args0))%expr @ + (##(- + (let + (x8, _) := + xv in + x8))%Z)%expr)))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v2)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v2)))%expr_pat))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2497,33 +2730,46 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with - ZRange.normalize args3)%zrange then Datatypes.Some - (UnderLet - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - (#(Z_sub_with_get_borrow)%expr @ - v (Compile.reflect x3) @ - (#(Z_cast args1)%expr @ - v0 (Compile.reflect x6)) @ - v1 (Compile.reflect x1) @ - (#(Z_cast (- args0))%expr @ - (##(- (let (x8, _) := xv in x8))%Z)%expr)))%expr_pat - (fun v2 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - ($v2)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (- - (#(Z_cast (- Datatypes.snd range))%expr @ - (#(snd)%expr @ - (#(Z_cast2 - (Datatypes.fst range, - - Datatypes.snd range))%expr @ - $v2)))%expr_pat)%expr)%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false + (expr_let v2 := (#(Z_cast2 + (Datatypes.fst + range, + - + Datatypes.snd + range))%expr @ + (#(Z_sub_with_get_borrow)%expr @ + ($(v + (Compile.reflect + x3)))%expr @ + (#(Z_cast args1)%expr @ + ($(v0 + (Compile.reflect + x6)))%expr) @ + ($(v1 + (Compile.reflect + x1)))%expr @ + (#(Z_cast (- args0))%expr @ + (##(- + (let + (x8, _) := + xv in + x8))%Z)%expr)))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v2)), + #(Z_cast (Datatypes.snd range))%expr @ + (- + (#(Z_cast (- Datatypes.snd range))%expr @ + (#(snd)%expr @ + (#(Z_cast2 + (Datatypes.fst range, + - Datatypes.snd range))%expr @ + $v2)))%expr_pat))%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -2603,26 +2849,29 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x8, _) := xv1 in x8) =? 0) then Datatypes.Some - (UnderLet - (#(Z_cast2 range)%expr @ - (#(Z_add_with_get_carry)%expr @ - (#(Z_cast args4)%expr @ - (##(let (x8, _) := xv in x8))%expr) @ - (#(Z_cast args5)%expr @ - v (Compile.reflect x4)) @ - (#(Z_cast args2)%expr @ - (##0)%expr) @ - (#(Z_cast args0)%expr @ - (##0)%expr)))%expr_pat - (fun v0 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast - (Datatypes.fst range))%expr @ - (#(fst)%expr @ - (#(Z_cast2 range)%expr @ - ($v0)%expr)), - #(Z_cast r[0 ~> 0])%expr @ - (##0)%expr)%expr_pat)) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false + (expr_let v0 := (#(Z_cast2 range)%expr @ + (#(Z_add_with_get_carry)%expr @ + (#(Z_cast args4)%expr @ + (##(let + (x8, + _) := + xv in + x8))%expr) @ + (#(Z_cast args5)%expr @ + ($(v + (Compile.reflect + x4)))%expr) @ + (#(Z_cast args2)%expr @ + (##0)%expr) @ + (#(Z_cast args0)%expr @ + (##0)%expr)))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ + (#(Z_cast2 range)%expr @ $v0)), + #(Z_cast r[0 ~> 0])%expr @ ##0)%expr_pat)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -2672,17 +2921,19 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v1 <- type.try_make_transport_cps s0 ℤ; v2 <- type.try_make_transport_cps s ℤ; Datatypes.Some - (UnderLet - (#(Z_cast2 range)%expr @ - (#(Z_add_with_get_carry)%expr @ v (Compile.reflect x3) @ - v0 (Compile.reflect x2) @ v1 (Compile.reflect x1) @ - v2 (Compile.reflect x0)))%expr_pat - (fun v3 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ (#(Z_cast2 range)%expr @ ($v3)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (#(snd)%expr @ (#(Z_cast2 range)%expr @ ($v3)%expr)))%expr_pat)) + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v3 := (#(Z_cast2 range)%expr @ + (#(Z_add_with_get_carry)%expr @ + ($(v (Compile.reflect x3)))%expr @ + ($(v0 (Compile.reflect x2)))%expr @ + ($(v1 (Compile.reflect x1)))%expr @ + ($(v2 (Compile.reflect x0)))%expr))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ (#(Z_cast2 range)%expr @ $v3)), + #(Z_cast (Datatypes.snd range))%expr @ + (#(snd)%expr @ (#(Z_cast2 range)%expr @ $v3)))%expr_pat); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end);; @@ -2701,17 +2952,19 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v1 <- type.try_make_transport_cps s0 ℤ; v2 <- type.try_make_transport_cps s ℤ; Datatypes.Some - (UnderLet - (#(Z_cast2 range)%expr @ - (#(Z_sub_with_get_borrow)%expr @ v (Compile.reflect x3) @ - v0 (Compile.reflect x2) @ v1 (Compile.reflect x1) @ - v2 (Compile.reflect x0)))%expr_pat - (fun v3 : var (ℤ * ℤ)%etype => - Base - (#(Z_cast (Datatypes.fst range))%expr @ - (#(fst)%expr @ (#(Z_cast2 range)%expr @ ($v3)%expr)), - #(Z_cast (Datatypes.snd range))%expr @ - (#(snd)%expr @ (#(Z_cast2 range)%expr @ ($v3)%expr)))%expr_pat)) + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (expr_let v3 := (#(Z_cast2 range)%expr @ + (#(Z_sub_with_get_borrow)%expr @ + ($(v (Compile.reflect x3)))%expr @ + ($(v0 (Compile.reflect x2)))%expr @ + ($(v1 (Compile.reflect x1)))%expr @ + ($(v2 (Compile.reflect x0)))%expr))%expr_pat in + (#(Z_cast (Datatypes.fst range))%expr @ + (#(fst)%expr @ (#(Z_cast2 range)%expr @ $v3)), + #(Z_cast (Datatypes.snd range))%expr @ + (#(snd)%expr @ (#(Z_cast2 range)%expr @ $v3)))%expr_pat); + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end diff --git a/src/fancy_rewrite_head.out b/src/fancy_rewrite_head.out index d0c555ca2..104ad09b3 100644 --- a/src/fancy_rewrite_head.out +++ b/src/fancy_rewrite_head.out @@ -47,6 +47,26 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with to_expr (x0 ($x3) (fun x6 : expr P => Base ($x4 @ x6)%expr_pat) ($x5)))%expr @ x1 @ x2)%expr_pat +| @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)) @@ -56,6 +76,43 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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 +| @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 + (#(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 +| @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)) @@ -114,6 +171,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | @List_nth_default T => fun (x : expr T) (x0 : expr (list T)) (x1 : expr ℕ) => Base (#(List_nth_default)%expr @ x @ x0 @ x1)%expr_pat +| @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 ℤ => Base (x + x0)%expr | Z_mul => fun x x0 : expr ℤ => Base (x * x0)%expr | Z_pow => fun x x0 : expr ℤ => Base (#(Z_pow)%expr @ x @ x0)%expr_pat @@ -165,6 +225,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fun x x0 x1 x2 : expr ℤ => Base (#(Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat | Z_cc_m => fun x x0 : expr ℤ => Base (#(Z_cc_m)%expr @ x @ x0)%expr_pat +| Z_combine_at_bitwidth => + fun x x0 x1 : expr ℤ => + Base (#(Z_combine_at_bitwidth)%expr @ x @ x0 @ x1)%expr_pat | 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 diff --git a/src/fancy_with_casts_rewrite_head.out b/src/fancy_with_casts_rewrite_head.out index bef104fd0..e493afa78 100644 --- a/src/fancy_with_casts_rewrite_head.out +++ b/src/fancy_with_casts_rewrite_head.out @@ -47,6 +47,26 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with to_expr (x0 ($x3) (fun x6 : expr P => Base ($x4 @ x6)%expr_pat) ($x5)))%expr @ x1 @ x2)%expr_pat +| @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)) @@ -56,6 +76,43 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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 +| @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 + (#(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 +| @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)) @@ -114,6 +171,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | @List_nth_default T => fun (x : expr T) (x0 : expr (list T)) (x1 : expr ℕ) => Base (#(List_nth_default)%expr @ x @ x0 @ x1)%expr_pat +| @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 ℤ => Base (x + x0)%expr | Z_mul => fun x x0 : expr ℤ => Base (x * x0)%expr | Z_pow => fun x x0 : expr ℤ => Base (#(Z_pow)%expr @ x @ x0)%expr_pat @@ -169,7 +229,12 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with type.type_beq base.type base.type.type_beq ((ℤ -> ℤ) -> ℤ)%ptype ((ℤ -> ℤ) -> ℤ)%ptype then - Datatypes.Some (Base (#(fancy_addm)%expr @ (x, x0, x1))%expr_pat) + Datatypes.Some + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (#(fancy_addm)%expr @ + (($x)%expr, ($x0)%expr, ($x1)%expr))%expr_pat; + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end;;; @@ -178,6 +243,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fun x x0 x1 x2 : expr ℤ => Base (#(Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat | Z_cc_m => fun x x0 : expr ℤ => Base (#(Z_cc_m)%expr @ x @ x0)%expr_pat +| Z_combine_at_bitwidth => + fun x x0 x1 : expr ℤ => + Base (#(Z_combine_at_bitwidth)%expr @ x @ x0 @ x1)%expr_pat | Z_cast range => fun x : expr ℤ => ((match x with @@ -241,7 +309,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args3)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mulll (2 * @@ -259,7 +329,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | Datatypes.None => 0 end)%expr, #(Z_cast args1)%expr @ - v (Compile.reflect x6))))%expr_pat) + ($(v (Compile.reflect x6)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -320,7 +390,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args3)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mulll (2 * @@ -338,7 +410,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | Datatypes.None => 0 end)%expr, #(Z_cast args0)%expr @ - v (Compile.reflect x7))))%expr_pat) + ($(v (Compile.reflect x7)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -395,7 +467,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args3)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mulhl (2 * @@ -413,7 +487,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | Datatypes.None => 0 end)%expr, #(Z_cast args0)%expr @ - v (Compile.reflect x7))))%expr_pat) + ($(v (Compile.reflect x7)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -474,7 +548,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args3)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mulhl (2 * @@ -492,7 +568,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | Datatypes.None => 0 end)%expr, #(Z_cast args1)%expr @ - v (Compile.reflect x6))))%expr_pat) + ($(v (Compile.reflect x6)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -558,7 +634,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args3)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false (#(Z_cast range)%expr @ (#(fancy_mullh (2 * (let (x8, _) := xv0 in x8)))%expr @ @@ -572,7 +649,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | Datatypes.None => 0 end)%expr, #(Z_cast args1)%expr @ - v (Compile.reflect x6))))%expr_pat) + ($(v (Compile.reflect x6)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -619,7 +696,8 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args3)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false (#(Z_cast range)%expr @ (#(fancy_mulhh (2 * (let (x8, _) := xv0 in x8)))%expr @ @@ -632,7 +710,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | Datatypes.None => 0 end)%expr, #(Z_cast args1)%expr @ - v (Compile.reflect x6))))%expr_pat) + ($(v (Compile.reflect x6)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -790,14 +868,16 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args5)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mulll (2 * Z.log2_up (let (x8, _) := xv in x8)))%expr @ (#(Z_cast args1)%expr @ - v (Compile.reflect x6), + ($(v (Compile.reflect x6)))%expr, (##match invert_low (2 * @@ -891,14 +971,16 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args5)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mulll (2 * Z.log2_up (let (x8, _) := xv in x8)))%expr @ (#(Z_cast args3)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, (##match invert_low (2 * @@ -984,14 +1066,16 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args5)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mullh (2 * Z.log2_up (let (x8, _) := xv in x8)))%expr @ (#(Z_cast args2)%expr @ - v (Compile.reflect x6), + ($(v (Compile.reflect x6)))%expr, (##match invert_high (2 * @@ -1077,14 +1161,16 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args5)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mullh (2 * Z.log2_up (let (x8, _) := xv in x8)))%expr @ (#(Z_cast args3)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, (##match invert_high (2 * @@ -1182,7 +1268,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args3)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mulll (2 * @@ -1190,9 +1278,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (let (x12, _) := xv in x12)))%expr @ (#(Z_cast args5)%expr @ - v (Compile.reflect x6), + ($(v (Compile.reflect x6)))%expr, #(Z_cast args)%expr @ - v0 (Compile.reflect x11))))%expr_pat) + ($(v0 (Compile.reflect x11)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -1360,7 +1448,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args3)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mulll (2 * @@ -1368,9 +1458,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (let (x12, _) := xv in x12)))%expr @ (#(Z_cast args6)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, #(Z_cast args)%expr @ - v0 (Compile.reflect x11))))%expr_pat) + ($(v0 (Compile.reflect x11)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -1537,7 +1627,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args3)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mulll (2 * @@ -1545,9 +1637,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (let (x12, _) := xv in x12)))%expr @ (#(Z_cast args5)%expr @ - v (Compile.reflect x6), + ($(v (Compile.reflect x6)))%expr, #(Z_cast args1)%expr @ - v0 (Compile.reflect x10))))%expr_pat) + ($(v0 (Compile.reflect x10)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -1712,7 +1804,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args3)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mulll (2 * @@ -1720,9 +1814,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (let (x12, _) := xv in x12)))%expr @ (#(Z_cast args6)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, #(Z_cast args1)%expr @ - v0 (Compile.reflect x10))))%expr_pat) + ($(v0 (Compile.reflect x10)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -1879,16 +1973,18 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args3)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mullh (2 * (let (x12, _) := xv0 in x12)))%expr @ (#(Z_cast args5)%expr @ - v (Compile.reflect x6), + ($(v (Compile.reflect x6)))%expr, #(Z_cast args1)%expr @ - v0 (Compile.reflect x10))))%expr_pat) + ($(v0 (Compile.reflect x10)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -2045,16 +2141,18 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args3)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mullh (2 * (let (x12, _) := xv0 in x12)))%expr @ (#(Z_cast args6)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, #(Z_cast args1)%expr @ - v0 (Compile.reflect x10))))%expr_pat) + ($(v0 (Compile.reflect x10)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -2212,12 +2310,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args5)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mulhl (2 * (let (x8, _) := xv in x8)))%expr @ (#(Z_cast args3)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, (##match invert_low (2 * @@ -2276,12 +2376,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args5)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast range)%expr @ (#(fancy_mulhh (2 * (let (x8, _) := xv in x8)))%expr @ (#(Z_cast args3)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, (##match invert_high (2 * @@ -2375,7 +2477,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args3)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota + var) false (#(Z_cast range)%expr @ (#(fancy_mulhl (2 * @@ -2383,10 +2487,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv in x12)))%expr @ (#(Z_cast args6)%expr @ - v (Compile.reflect x5), + ($(v + (Compile.reflect + x5)))%expr, #(Z_cast args)%expr @ - v0 - (Compile.reflect x11))))%expr_pat) + ($(v0 + (Compile.reflect + x11)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -2462,16 +2569,18 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args3)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota + var) false (#(Z_cast range)%expr @ (#(fancy_mulhl (2 * (let (x12, _) := xv in x12)))%expr @ (#(Z_cast args6)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, #(Z_cast args1)%expr @ - v0 (Compile.reflect x10))))%expr_pat) + ($(v0 (Compile.reflect x10)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -2551,16 +2660,18 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args3)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota + var) false (#(Z_cast range)%expr @ (#(fancy_mulhh (2 * (let (x12, _) := xv in x12)))%expr @ (#(Z_cast args6)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, #(Z_cast args1)%expr @ - v0 (Compile.reflect x10))))%expr_pat) + ($(v0 (Compile.reflect x10)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -2718,7 +2829,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ZRange.normalize args5)%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota + var) false (#(Z_cast range)%expr @ (#(fancy_selm (Z.log2 @@ -2726,11 +2839,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv in x10)))%expr @ (#(Z_cast args1)%expr @ - v (Compile.reflect x7), + ($(v (Compile.reflect x7)))%expr, #(Z_cast args0)%expr @ - v0 (Compile.reflect x8), + ($(v0 (Compile.reflect x8)))%expr, #(Z_cast args)%expr @ - v1 (Compile.reflect x9))))%expr_pat) + ($(v1 (Compile.reflect x9)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -2821,15 +2934,23 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 1) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota + var) false (#(Z_cast range)%expr @ (#(fancy_sell)%expr @ (#(Z_cast args1)%expr @ - v (Compile.reflect x7), + ($(v + (Compile.reflect + x7)))%expr, #(Z_cast args0)%expr @ - v0 (Compile.reflect x8), + ($(v0 + (Compile.reflect + x8)))%expr, #(Z_cast args)%expr @ - v1 (Compile.reflect x9))))%expr_pat) + ($(v1 + (Compile.reflect + x9)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -2902,15 +3023,17 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with ((let (x10, _) := xv in x10) =? 1) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota + var) false (#(Z_cast range)%expr @ (#(fancy_sell)%expr @ (#(Z_cast args3)%expr @ - v (Compile.reflect x6), + ($(v (Compile.reflect x6)))%expr, #(Z_cast args0)%expr @ - v0 (Compile.reflect x8), + ($(v0 (Compile.reflect x8)))%expr, #(Z_cast args)%expr @ - v1 (Compile.reflect x9))))%expr_pat) + ($(v1 (Compile.reflect x9)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -2972,11 +3095,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- type.try_make_transport_cps s0 ℤ; v1 <- type.try_make_transport_cps s ℤ; Datatypes.Some - (Base - (#(Z_cast range)%expr @ - (#(fancy_selc)%expr @ - (v (Compile.reflect x2), v0 (Compile.reflect x1), - v1 (Compile.reflect x0))))%expr_pat) + (fv <-- Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (#(Z_cast range)%expr @ + (#(fancy_selc)%expr @ + (($(v (Compile.reflect x2)))%expr, + ($(v0 (Compile.reflect x1)))%expr, + ($(v1 (Compile.reflect x0)))%expr)))%expr_pat; + Base fv)%under_lets else Datatypes.None | Datatypes.None => Datatypes.None end @@ -3018,12 +3144,15 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 2 ^ Z.log2 (let (x8, _) := xv in x8)) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false (#(Z_cast range)%expr @ (#(fancy_rshi (Z.log2 (let (x8, _) := xv in x8)) (let (x8, _) := xv0 in x8))%expr @ - (#(Z_cast args2)%expr @ v (Compile.reflect x5), - #(Z_cast args1)%expr @ v0 (Compile.reflect x6))))%expr_pat) + (#(Z_cast args2)%expr @ + ($(v (Compile.reflect x5)))%expr, + #(Z_cast args1)%expr @ + ($(v0 (Compile.reflect x6)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -3304,7 +3433,10 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (range <=? value_range)%zrange || (range <=? flag_range)%zrange then - Datatypes.Some (Base (#(Z_cast range)%expr @ x)%expr_pat) + Datatypes.Some + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + (#(Z_cast range)%expr @ ($x)%expr)%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -3402,7 +3534,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with Z.log2 (let (x14, _) := xv in x14))) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast2 range)%expr @ (#(fancy_add (Z.log2 @@ -3411,9 +3545,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (let (x14, _) := xv1 in x14))%expr @ (#(Z_cast args8)%expr @ - v (Compile.reflect x4), + ($(v (Compile.reflect x4)))%expr, #(Z_cast args3)%expr @ - v0 (Compile.reflect x11))))%expr_pat) + ($(v0 (Compile.reflect x11)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -3490,7 +3624,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 1])%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast2 range)%expr @ (#(fancy_add (Z.log2 @@ -3498,9 +3634,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with x14)) (let (x14, _) := xv1 in x14))%expr @ (#(Z_cast args8)%expr @ - v (Compile.reflect x4), + ($(v (Compile.reflect x4)))%expr, #(Z_cast args3)%expr @ - v0 (Compile.reflect x11))))%expr_pat) + ($(v0 (Compile.reflect x11)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -3801,7 +3937,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with Z.log2 (let (x14, _) := xv in x14))) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast2 range)%expr @ (#(fancy_add (Z.log2 @@ -3809,9 +3947,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with x14)) (let (x14, _) := xv1 in x14))%expr @ (#(Z_cast args7)%expr @ - v0 (Compile.reflect x5), + ($(v0 (Compile.reflect x5)))%expr, #(Z_cast args3)%expr @ - v (Compile.reflect x11))))%expr_pat) + ($(v (Compile.reflect x11)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -4084,7 +4222,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 1])%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast2 range)%expr @ (#(fancy_add (Z.log2 @@ -4094,9 +4234,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (let (x10, _) := xv0 in x10)))%expr @ (#(Z_cast args4)%expr @ - v (Compile.reflect x4), + ($(v (Compile.reflect x4)))%expr, #(Z_cast args1)%expr @ - v0 (Compile.reflect x8))))%expr_pat) + ($(v0 (Compile.reflect x8)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -4206,7 +4346,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 1])%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast2 range)%expr @ (#(fancy_add (Z.log2 @@ -4216,9 +4358,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (let (x10, _) := xv0 in x10)))%expr @ (#(Z_cast args3)%expr @ - v0 (Compile.reflect x5), + ($(v0 (Compile.reflect x5)))%expr, #(Z_cast args1)%expr @ - v (Compile.reflect x8))))%expr_pat) + ($(v (Compile.reflect x8)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -4305,15 +4447,17 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with r[0 ~> (let (x6, _) := xv in x6) - 1])%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast2 range)%expr @ (#(fancy_add (Z.log2 (let (x6, _) := xv in x6)) 0)%expr @ (#(Z_cast args0)%expr @ - v (Compile.reflect x4), + ($(v (Compile.reflect x4)))%expr, #(Z_cast args)%expr @ - v0 (Compile.reflect x5))))%expr_pat) + ($(v0 (Compile.reflect x5)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -4453,7 +4597,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (let (x14, _) := xv in x14))) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota + var) false (#(Z_cast2 range)%expr @ (#(fancy_sub (Z.log2 @@ -4464,10 +4610,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv1 in x14))%expr @ (#(Z_cast args8)%expr @ - v (Compile.reflect x4), + ($(v + (Compile.reflect + x4)))%expr, #(Z_cast args3)%expr @ - v0 - (Compile.reflect x11))))%expr_pat) + ($(v0 + (Compile.reflect + x11)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -4642,7 +4791,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with x10) - 1])%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota + var) false (#(Z_cast2 range)%expr @ (#(fancy_sub (Z.log2 @@ -4654,9 +4805,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 in x10)))%expr @ (#(Z_cast args4)%expr @ - v (Compile.reflect x4), + ($(v + (Compile.reflect + x4)))%expr, #(Z_cast args1)%expr @ - v0 (Compile.reflect x8))))%expr_pat) + ($(v0 + (Compile.reflect + x8)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -4709,15 +4864,17 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with r[0 ~> (let (x6, _) := xv in x6) - 1])%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast2 range)%expr @ (#(fancy_sub (Z.log2 (let (x6, _) := xv in x6)) 0)%expr @ (#(Z_cast args0)%expr @ - v (Compile.reflect x4), + ($(v (Compile.reflect x4)))%expr, #(Z_cast args)%expr @ - v0 (Compile.reflect x5))))%expr_pat) + ($(v0 (Compile.reflect x5)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets @@ -4844,7 +5001,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (let (x16, _) := xv in x16))) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota + var) false (#(Z_cast2 range)%expr @ (#(fancy_addc (Z.log2 @@ -4854,11 +5013,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (let (x16, _) := xv1 in x16))%expr @ (#(Z_cast args9)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, #(Z_cast args8)%expr @ - v0 (Compile.reflect x6), + ($(v0 (Compile.reflect x6)))%expr, #(Z_cast args3)%expr @ - v1 (Compile.reflect x13))))%expr_pat) + ($(v1 (Compile.reflect x13)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -5180,7 +5339,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (let (x16, _) := xv in x16))) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota + var) false (#(Z_cast2 range)%expr @ (#(fancy_addc (Z.log2 @@ -5190,11 +5351,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (let (x16, _) := xv1 in x16))%expr @ (#(Z_cast args9)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, #(Z_cast args7)%expr @ - v1 (Compile.reflect x7), + ($(v1 (Compile.reflect x7)))%expr, #(Z_cast args3)%expr @ - v0 (Compile.reflect x13))))%expr_pat) + ($(v0 (Compile.reflect x13)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -5482,7 +5643,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 1])%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota + var) false (#(Z_cast2 range)%expr @ (#(fancy_addc (Z.log2 @@ -5494,11 +5657,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 in x12)))%expr @ (#(Z_cast args5)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, #(Z_cast args4)%expr @ - v0 (Compile.reflect x6), + ($(v0 (Compile.reflect x6)))%expr, #(Z_cast args1)%expr @ - v1 (Compile.reflect x10))))%expr_pat) + ($(v1 (Compile.reflect x10)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -5616,7 +5779,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 1])%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota + var) false (#(Z_cast2 range)%expr @ (#(fancy_addc (Z.log2 @@ -5628,11 +5793,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 in x12)))%expr @ (#(Z_cast args5)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, #(Z_cast args3)%expr @ - v1 (Compile.reflect x7), + ($(v1 (Compile.reflect x7)))%expr, #(Z_cast args1)%expr @ - v0 (Compile.reflect x10))))%expr_pat) + ($(v0 (Compile.reflect x10)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -5725,18 +5890,20 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with r[0 ~> (let (x8, _) := xv in x8) - 1])%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast2 range)%expr @ (#(fancy_addc (Z.log2 (let (x8, _) := xv in x8)) 0)%expr @ (#(Z_cast args1)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, #(Z_cast args0)%expr @ - v0 (Compile.reflect x6), + ($(v0 (Compile.reflect x6)))%expr, #(Z_cast args)%expr @ - v1 (Compile.reflect x7))))%expr_pat) + ($(v1 (Compile.reflect x7)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -5905,7 +6072,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with x16))) then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota + var) false (#(Z_cast2 range)%expr @ (#(fancy_subb (Z.log2 @@ -5919,17 +6088,17 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv1 in x16))%expr @ (#(Z_cast args9)%expr @ - v - (Compile.reflect - x5), + ($(v + (Compile.reflect + x5)))%expr, #(Z_cast args8)%expr @ - v0 - (Compile.reflect - x6), + ($(v0 + (Compile.reflect + x6)))%expr, #(Z_cast args3)%expr @ - v1 - (Compile.reflect - x13))))%expr_pat) + ($(v1 + (Compile.reflect + x13)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -6120,7 +6289,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with x12) - 1])%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota + var) false (#(Z_cast2 range)%expr @ (#(fancy_subb (Z.log2 @@ -6135,17 +6306,17 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with xv0 in x12)))%expr @ (#(Z_cast args5)%expr @ - v - (Compile.reflect - x5), + ($(v + (Compile.reflect + x5)))%expr, #(Z_cast args4)%expr @ - v0 - (Compile.reflect - x6), + ($(v0 + (Compile.reflect + x6)))%expr, #(Z_cast args1)%expr @ - v1 - (Compile.reflect - x10))))%expr_pat) + ($(v1 + (Compile.reflect + x10)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; @@ -6205,18 +6376,20 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with r[0 ~> (let (x8, _) := xv in x8) - 1])%zrange then Datatypes.Some - (Base + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) + false (#(Z_cast2 range)%expr @ (#(fancy_subb (Z.log2 (let (x8, _) := xv in x8)) 0)%expr @ (#(Z_cast args1)%expr @ - v (Compile.reflect x5), + ($(v (Compile.reflect x5)))%expr, #(Z_cast args0)%expr @ - v0 (Compile.reflect x6), + ($(v0 (Compile.reflect x6)))%expr, #(Z_cast args)%expr @ - v1 (Compile.reflect x7))))%expr_pat) + ($(v1 (Compile.reflect x7)))%expr)))%expr_pat) else Datatypes.None); Datatypes.Some (fv0 <-- fv; diff --git a/src/nbe_rewrite_head.out b/src/nbe_rewrite_head.out index 9c3922844..ef9e829f3 100644 --- a/src/nbe_rewrite_head.out +++ b/src/nbe_rewrite_head.out @@ -238,7 +238,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with _ <- 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 (Base (v4 (v3 (v1 (v (Compile.reflect x1)))))) + 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 @@ -291,7 +295,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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 (Base (v4 (v3 (v2 (v0 (Compile.reflect x0)))))) + 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 @@ -356,10 +364,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v3 <- base.try_make_transport_cps b7 T; v4 <- base.try_make_transport_cps T T; Datatypes.Some - (fv1 <-- (e <-- x'4 (x'3 (x'2 (x'1 (x'0 (x' x))))) - (v1 (v (Compile.reflect x2))) - (v2 (v0 (Compile.reflect x1))); - Base e); + (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 @@ -413,8 +422,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fv0 <- (if let (x2, _) := xv in x2 then Datatypes.Some - (e <-- x'1 (x' x) (##tt)%expr; - Base e)%under_lets + (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 @@ -451,8 +461,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with then Datatypes.None else Datatypes.Some - (e <-- x'2 (x'0 x0) (##tt)%expr; - Base e)%under_lets); + (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 @@ -500,13 +511,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- base.try_make_transport_cps b10 P; v0 <- base.try_make_transport_cps P P; Datatypes.Some - (fv0 <-- Datatypes.nat_rect - (fun _ : nat => UnderLets (expr b10)) - (x'2 (x' x) (##tt)%expr) - (fun (n' : nat) (rec : UnderLets (expr b10)) => - rec0 <-- rec; - x'4 (x'3 (x'1 (x'0 x0))) (##n')%expr rec0) - (let (x2, _) := xv in x2); + (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 @@ -568,15 +577,14 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v1 <- base.try_make_transport_cps b16 Q; v2 <- base.try_make_transport_cps Q Q; Datatypes.Some - (fv0 <-- Datatypes.nat_rect - (fun _ : nat => expr b -> UnderLets (expr b16)) - (x'6 (x'5 (x'0 (x' x)))) - (fun (n' : nat) - (rec : expr b -> UnderLets (expr b16)) - (v3 : expr b) => - x'10 (x'9 (x'8 (x'7 (x'4 (x'3 (x'2 (x'1 x0))))))) - (##n')%expr rec v3) (let (x3, _) := xv in x3) - (v0 (v x2)); + (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 @@ -590,6 +598,26 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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)) @@ -631,18 +659,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- base.try_make_transport_cps b b; v1 <- base.try_make_transport_cps b12 P; v2 <- base.try_make_transport_cps P P; - fv0 <- (ls <- reflect_list (v0 (v x1)); - Datatypes.Some - (Datatypes.list_rect - (fun _ : Datatypes.list (expr b) => - UnderLets (expr b12)) (x'4 (x' x) (##tt)%expr) - (fun (x2 : expr b) (xs : Datatypes.list (expr b)) - (rec : UnderLets (expr b12)) => - (rec' <-- rec; - x'8 (x'7 (x'6 (x'5 (x'3 (x'2 (x'1 (x'0 x0))))))) x2 - (Compilers.reify_list xs) rec')%under_lets) ls)); - Datatypes.Some (fv1 <-- fv0; - Base (v2 (v1 fv1)))%under_lets + 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;; @@ -652,6 +675,117 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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)) @@ -693,8 +827,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v <- base.try_make_transport_cps b10 P; v0 <- base.try_make_transport_cps P P; Datatypes.Some - (fv0 <-- (e <-- x'3 (x' x) (##tt)%expr; - Base e); + (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 @@ -746,10 +881,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v3 <- base.try_make_transport_cps b10 P; v4 <- base.try_make_transport_cps P P; Datatypes.Some - (fv1 <-- (e <-- x'6 (x'5 (x'4 (x'2 (x'1 (x'0 x0))))) - (v1 (v (Compile.reflect x3))) - (v2 (v0 (Compile.reflect x2))); - Base e); + (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 @@ -773,28 +909,34 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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; - fv0 <- (x0 <- (xs <- reflect_list (v0 (v x)); - Datatypes.Some (##(length xs))%expr); - Datatypes.Some (Base x0)); - Datatypes.Some (fv1 <-- fv0; - Base fv1)%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end;;; + ((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 ℕ => @@ -854,13 +996,24 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- base.try_make_transport_cps b b; v1 <- base.try_make_transport_cps b A; v2 <- base.try_make_transport_cps A A; - fv0 <- (xs <- reflect_list (v0 (v x0)); - Datatypes.Some - (Base - (Compilers.reify_list - (firstn (let (x1, _) := xv in x1) xs)))); - Datatypes.Some (fv1 <-- fv0; - Base (v2 (v1 fv1)))%under_lets + 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 @@ -892,13 +1045,24 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- base.try_make_transport_cps b b; v1 <- base.try_make_transport_cps b A; v2 <- base.try_make_transport_cps A A; - fv0 <- (xs <- reflect_list (v0 (v x0)); - Datatypes.Some - (Base - (Compilers.reify_list - (skipn (let (x1, _) := xv in x1) xs)))); - Datatypes.Some (fv1 <-- fv0; - Base (v2 (v1 fv1)))%under_lets + 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 @@ -929,11 +1093,15 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v1 <- base.try_make_transport_cps b0 A; v2 <- base.try_make_transport_cps A A; Datatypes.Some - (Base - (v2 - (v1 - (Compilers.reify_list - (repeat (v0 (v x)) (let (x1, _) := xv in x1)))))) + (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 @@ -943,44 +1111,55 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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; - fv0 <- (x1 <- (xs <- reflect_list (v1 (v x)); - ys <- reflect_list (v2 (v0 x0)); - Datatypes.Some - (Compilers.reify_list - (List.map - (fun '(x1, y)%zrange => (x1, y)%expr_pat) - (List.combine xs ys)))); - Datatypes.Some (Base x1)); - Datatypes.Some - (fv1 <-- fv0; - Base (x'2 (x'1 (x'0 (x' fv1)))))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end;;; + ((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)) => @@ -1006,18 +1185,17 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- base.try_make_transport_cps b b; v1 <- base.try_make_transport_cps b4 B; v2 <- base.try_make_transport_cps B B; - fv0 <- (ls <- reflect_list (v0 (v x0)); - Datatypes.Some - (Datatypes.list_rect - (fun _ : Datatypes.list (expr b) => - UnderLets (expr (list b4))) (Base []%expr_pat) - (fun (x1 : expr b) (_ : Datatypes.list (expr b)) - (rec : UnderLets (expr (list b4))) => - (rec' <-- rec; - fx <-- x'2 (x'1 (x'0 (x' x))) x1; - Base (fx :: rec')%expr_pat)%under_lets) ls)); - Datatypes.Some (fv1 <-- fv0; - Base (v2 (v1 fv1)))%under_lets + 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;; @@ -1047,17 +1225,15 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v2 <- base.try_make_transport_cps b b; v3 <- base.try_make_transport_cps b A; v4 <- base.try_make_transport_cps A A; - fv0 <- (ls <- reflect_list (v1 (v x)); - Datatypes.Some - (Datatypes.list_rect - (fun _ : Datatypes.list (expr b) => - UnderLets (expr (list b))) (Base (v2 (v0 x0))) - (fun (x1 : expr b) (_ : Datatypes.list (expr b)) - (rec : UnderLets (expr (list b))) => - (rec' <-- rec; - Base (x1 :: rec')%expr_pat)%under_lets) ls)); - Datatypes.Some (fv1 <-- fv0; - Base (v4 (v3 fv1)))%under_lets + 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;; @@ -1065,31 +1241,36 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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; - fv0 <- (xs <- reflect_list (v0 (v x)); - Datatypes.Some (Base (Compilers.reify_list (rev xs)))); - Datatypes.Some (fv1 <-- fv0; - Base (v2 (v1 fv1)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end;; - Datatypes.None);;; + (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)) => @@ -1119,20 +1300,18 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- base.try_make_transport_cps b b; v1 <- base.try_make_transport_cps b4 B; v2 <- base.try_make_transport_cps B B; - fv0 <- (ls <- reflect_list (v0 (v x0)); - Datatypes.Some - (Datatypes.list_rect - (fun _ : Datatypes.list (expr b) => - UnderLets (expr (list b4))) (Base []%expr_pat) - (fun (x1 : expr b) (_ : Datatypes.list (expr b)) - (rec : UnderLets (expr (list b4))) => - (rec' <-- rec; - fx <-- x'2 (x'1 (x'0 (x' x))) x1; - Base ($fx ++ rec')%expr)%under_lets) ls)); Datatypes.Some - (fv1 <-- fv0; - fv2 <-- do_again (list B) (v1 fv1); - Base (v2 fv2))%under_lets + (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;; @@ -1142,60 +1321,55 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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; - fv0 <- (ls <- reflect_list (v0 (v x0)); - Datatypes.Some - (Datatypes.list_rect - (fun _ : Datatypes.list (expr b) => - UnderLets (expr (list b * list b)%etype)) - (Base ([], [])%expr_pat) - (fun (x1 : expr b) (_ : Datatypes.list (expr b)) - (rec : UnderLets (expr (list b * list b)%etype)) - => - (rec' <-- rec; - fx <-- x'0 (x' x) x1; - Base - (#(prod_rect)%expr @ - (λ g d : expr (list b), - (#(bool_rect)%expr @ - (λ _ : expr unit, - ($x1 :: $g, $d)%expr_pat) @ - (λ _ : expr unit, - ($g, $x1 :: $d)%expr_pat) @ $fx)%expr_pat)%expr @ - rec')%expr_pat)%under_lets) ls)); - Datatypes.Some - (fv1 <-- fv0; - fv2 <-- do_again (list A * list A) (x'2 (x'1 fv1)); - Base (x'4 (x'3 fv2)))%under_lets - else Datatypes.None - | Datatypes.None => Datatypes.None - end;; - Datatypes.None);;; + (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 @@ -1232,18 +1406,16 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v2 <- base.try_make_transport_cps b b; v3 <- base.try_make_transport_cps b0 A; v4 <- base.try_make_transport_cps A A; - fv0 <- (ls <- reflect_list (v2 (v0 x1)); - Datatypes.Some - (Datatypes.list_rect - (fun _ : Datatypes.list (expr b) => - UnderLets (expr b0)) (Base (v1 (v x0))) - (fun (x2 : expr b) (_ : Datatypes.list (expr b)) - (rec : UnderLets (expr b0)) => - (rec' <-- rec; - x'4 (x'3 (x'2 (x'1 (x'0 (x' x))))) x2 rec')%under_lets) - ls)); - Datatypes.Some (fv1 <-- fv0; - Base (v4 (v3 fv1)))%under_lets + 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;; @@ -1285,16 +1457,29 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v0 <- base.try_make_transport_cps b b; v1 <- base.try_make_transport_cps b T; v2 <- base.try_make_transport_cps T T; - fv0 <- (ls <- reflect_list (v0 (v x1)); - Datatypes.Some - (retv <---- update_nth (let (x2, _) := xv in x2) - (fun x2 : UnderLets (expr b) => - x3 <-- x2; - x'2 (x'1 (x'0 (x' x0))) x3) - (List.map Base ls); - Base (Compilers.reify_list retv))%under_lets); - Datatypes.Some (fv1 <-- fv0; - Base (v2 (v1 fv1)))%under_lets + 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 @@ -1331,13 +1516,13 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with v2 <- base.try_make_transport_cps b0 b0; v3 <- base.try_make_transport_cps b0 T; v4 <- base.try_make_transport_cps T T; - fv0 <- (x2 <- (ls <- reflect_list (v2 (v0 x0)); - Datatypes.Some - (nth_default (v1 (v x)) ls - (let (x2, _) := xv in x2))); - Datatypes.Some (Base x2)); - Datatypes.Some (fv1 <-- fv0; - Base (v4 (v3 fv1)))%under_lets + 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 @@ -1345,6 +1530,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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 @@ -2503,6 +2691,50 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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 diff --git a/src/strip_literal_casts_rewrite_head.out b/src/strip_literal_casts_rewrite_head.out index 916f44c85..9263d5f52 100644 --- a/src/strip_literal_casts_rewrite_head.out +++ b/src/strip_literal_casts_rewrite_head.out @@ -47,6 +47,26 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with to_expr (x0 ($x3) (fun x6 : expr P => Base ($x4 @ x6)%expr_pat) ($x5)))%expr @ x1 @ x2)%expr_pat +| @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)) @@ -56,6 +76,43 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with 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 +| @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 + (#(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 +| @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)) @@ -114,6 +171,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with | @List_nth_default T => fun (x : expr T) (x0 : expr (list T)) (x1 : expr ℕ) => Base (#(List_nth_default)%expr @ x @ x0 @ x1)%expr_pat +| @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 ℤ => Base (x + x0)%expr | Z_mul => fun x x0 : expr ℤ => Base (x * x0)%expr | Z_pow => fun x x0 : expr ℤ => Base (#(Z_pow)%expr @ x @ x0)%expr_pat @@ -165,6 +225,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with fun x x0 x1 x2 : expr ℤ => Base (#(Z_rshi)%expr @ x @ x0 @ x1 @ x2)%expr_pat | Z_cc_m => fun x x0 : expr ℤ => Base (#(Z_cc_m)%expr @ x @ x0)%expr_pat +| Z_combine_at_bitwidth => + fun x x0 x1 : expr ℤ => + Base (#(Z_combine_at_bitwidth)%expr @ x @ x0 @ x1)%expr_pat | Z_cast range => fun x : expr ℤ => (match x with @@ -180,7 +243,9 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (ZRange.normalize range) then Datatypes.Some - (Base (##(let (x0, _) := xv in x0))%expr) + (Reify.expr_value_to_rewrite_rule_replacement + (@Compile.reflect_ident_iota var) false + ##(let (x0, _) := xv in x0)) else Datatypes.None); Datatypes.Some (fv0 <-- fv; Base fv0)%under_lets |