diff options
author | Jason Gross <jagro@google.com> | 2018-07-26 19:28:52 -0400 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2018-07-26 19:28:52 -0400 |
commit | f2f418416535d91d9e7c7f6f083f898737adb9ee (patch) | |
tree | be26bff1fde4be4b106dbe7c9a194815153c758c /src | |
parent | 91b0b095de58548e927c28550db376692b692c5b (diff) |
Move the associator pass to the rewriter
This makes it somewhat more ad-hoc (we don't support arbitrary numbers
of multiplications), but it should hopefully be much easier to prove
things about.
Diffstat (limited to 'src')
-rw-r--r-- | src/Experiments/NewPipeline/CompilersTestCases.v | 22 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/MiscCompilerPasses.v | 64 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/README.md | 3 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/Rewriter.v | 34 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/Toplevel1.v | 6 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/arith_rewrite_head.out | 575 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/fancy_rewrite_head.out | 424 | ||||
-rw-r--r-- | src/Experiments/NewPipeline/nbe_rewrite_head.out | 478 |
8 files changed, 997 insertions, 609 deletions
diff --git a/src/Experiments/NewPipeline/CompilersTestCases.v b/src/Experiments/NewPipeline/CompilersTestCases.v index 3d8204fbf..2cd7880f3 100644 --- a/src/Experiments/NewPipeline/CompilersTestCases.v +++ b/src/Experiments/NewPipeline/CompilersTestCases.v @@ -219,7 +219,7 @@ Module test5. x) in pose v as E. vm_compute in E. - pose (ReassociateSmallConstants.Reassociate (2^8) (partial.Eval E)) as E'. + pose (RewriteRules.RewriteArith (2^8) (partial.Eval E)) as E'. lazy in E'. clear E. lazymatch (eval cbv delta [E'] in E') with @@ -231,6 +231,26 @@ Module test5. end. constructor. Qed. + + Example test5_2 : True. + Proof. + let v := Reify (fun y : (Z * Z) + => dlet_nd x := (2 * (19 * (fst y * snd y))) in + x) in + pose v as E. + vm_compute in E. + pose (RewriteRules.RewriteArith (2^8) (partial.Eval E)) as E'. + lazy in E'. + clear E. + lazymatch (eval cbv delta [E'] in E') with + | (fun var => + expr.Abs (fun v + => (expr_let v0 := (#ident.Z_mul @ (#ident.fst @ $v) @ (#ident.Z_mul @ (#ident.snd @ $v) @ (#ident.Z_mul @ #(ident.Literal 2) @ #(ident.Literal 19)))) in + $v0)%expr)) + => idtac + end. + constructor. + Qed. End test5. Module test6. (* check for no dead code with if *) diff --git a/src/Experiments/NewPipeline/MiscCompilerPasses.v b/src/Experiments/NewPipeline/MiscCompilerPasses.v index becce25d1..66dd7c09c 100644 --- a/src/Experiments/NewPipeline/MiscCompilerPasses.v +++ b/src/Experiments/NewPipeline/MiscCompilerPasses.v @@ -144,68 +144,4 @@ Module Compilers. := fun var => subst01 (ComputeLiveCounts e) (e _). End with_ident. End Subst01. - - Module ReassociateSmallConstants. - Section with_var. - Context (max_const_val : Z) - {var : type -> Type}. - - Local Notation tZ := (base.type.type_base base.type.Z). - Local Notation TZ := (type.base tZ). - Local Notation "x * y" := (expr.App (s:=TZ) (d:=TZ) (expr.App (s:=TZ) (d:=type.arrow TZ TZ) (expr.Ident ident.Z_mul) x) y) : expr_pat_scope. (* for patterns, for type inference *) - - Fixpoint to_mul_list (e : @expr var base.type.Z) : list (@expr var base.type.Z) - := match e in expr.expr t return list (@expr var t) with - | (x * y)%expr_pat => to_mul_list x ++ to_mul_list y - | expr.Var _ _ as e - | expr.Ident _ _ as e - | expr.LetIn _ _ _ _ as e - | expr.Abs _ _ _ as e - | expr.App _ _ _ _ as e - => [e] - end. - - Definition is_small_prim (e : @expr var base.type.Z) : bool - := match e with - | expr.Ident _ (ident.Literal base.type.Z v) - => Z.abs v <=? Z.abs max_const_val - | _ => false - end. - Definition is_not_small_prim (e : @expr var base.type.Z) : bool - := negb (is_small_prim e). - - Definition reorder_mul_list (ls : list (@expr var base.type.Z)) - : list (@expr var base.type.Z) - := filter is_not_small_prim ls ++ filter is_small_prim ls. - - Fixpoint of_mul_list (ls : list (@expr var base.type.Z)) : @expr var base.type.Z - := match ls with - | nil => ##1 - | cons x nil - => x - | cons x xs - => x * of_mul_list xs - end%expr_pat%expr. - - Fixpoint reassociate {t} (e : @expr var t) : @expr var t - := match e in expr.expr t return expr t with - | expr.Var _ _ as e - | expr.Ident _ _ as e - => e - | expr.App s d f x - => let reorder := match d return expr d -> expr d with - | type.base base.type.Z - => fun e => of_mul_list (reorder_mul_list (to_mul_list e)) - | _ => fun e => e - end in - reorder (expr.App (@reassociate _ f) (@reassociate _ x)) - | expr.Abs s d f => expr.Abs (fun v => @reassociate _ (f v)) - | expr.LetIn tx tC ex eC - => expr.LetIn (@reassociate tx ex) (fun v => @reassociate tC (eC v)) - end. - End with_var. - - Definition Reassociate (max_const_val : Z) {t} (e : Expr t) : Expr t - := fun var => reassociate max_const_val (e _). - End ReassociateSmallConstants. End Compilers. diff --git a/src/Experiments/NewPipeline/README.md b/src/Experiments/NewPipeline/README.md index 27c350ec8..e1b3b5b16 100644 --- a/src/Experiments/NewPipeline/README.md +++ b/src/Experiments/NewPipeline/README.md @@ -67,9 +67,6 @@ The files contain: - MiscCompilerPasses.v: Defines the passes: + EliminateDead (dead code elimination) + Subst01 (substitute let-binders used 0 or 1 times) - + ReassociateSmallConstants.Reassociate: - * (turn expressions of the form ((x * y) * ##v) into (x * (y * ##v)) for - small values of v) - CStringification.v: conversion to C code as strings. (Depends on AbstractInterpretation.v for ZRange utilities.) Defines the passes: diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v index 794dede40..5ebf429a1 100644 --- a/src/Experiments/NewPipeline/Rewriter.v +++ b/src/Experiments/NewPipeline/Rewriter.v @@ -1288,7 +1288,7 @@ In the RHS, the follow notation applies: reify_list retv)) ]%list%pattern%cps%option%under_lets%Z%bool. - Definition arith_rewrite_rules : rewrite_rulesT + Definition arith_rewrite_rules (max_const_val : Z) : rewrite_rulesT := [make_rewrite (#pattern.ident.fst @ (??, ??)) (fun _ x _ y => x) ; make_rewrite (#pattern.ident.snd @ (??, ??)) (fun _ x _ y => y) ; make_rewrite (#?ℤ + ??{ℤ}) (fun z v => v when Z.eqb z 0) @@ -1314,6 +1314,7 @@ In the RHS, the follow notation applies: ; make_rewrite ((-??{ℤ}) - ??{ℤ} ) (fun x y => -(x + y)) ; make_rewrite ( ??{ℤ} - (-??{ℤ})) (fun x y => x + y) + ; make_rewrite (#?ℤ * #?ℤ ) (fun x y => ##((x*y)%Z)) ; make_rewrite (#?ℤ * ??{ℤ}) (fun z v => ##0 when Z.eqb z 0) ; make_rewrite (??{ℤ} * #?ℤ ) (fun v z => ##0 when Z.eqb z 0) ; make_rewrite (#?ℤ * ??{ℤ}) (fun z v => v when Z.eqb z 1) @@ -1339,6 +1340,12 @@ In the RHS, the follow notation applies: ; make_rewrite (??{ℤ} mod #?ℤ) (fun x y => x &' ##(y-1)%Z when (y =? (2^Z.log2 y))) ; make_rewrite (-(-??{ℤ})) (fun v => v) + (* We reassociate some multiplication of small constants *) + ; make_rewrite (#?ℤ * (#?ℤ * (??{ℤ} * ??{ℤ}))) (fun c1 c2 x y => (x * (y * (##c1 * ##c2))) when (Z.abs c1 <=? Z.abs max_const_val) && (Z.abs c2 <=? Z.abs max_const_val)) + ; make_rewrite (#?ℤ * (??{ℤ} * (??{ℤ} * #?ℤ))) (fun c1 x y c2 => (x * (y * (##c1 * ##c2))) when (Z.abs c1 <=? Z.abs max_const_val) && (Z.abs c2 <=? Z.abs max_const_val)) + ; make_rewrite (#?ℤ * (??{ℤ} * ??{ℤ})) (fun c x y => (x * (y * ##c)) when (Z.abs c <=? Z.abs max_const_val)) + ; make_rewrite (#?ℤ * ??{ℤ}) (fun c x => (x * ##c) when (Z.abs c <=? Z.abs max_const_val)) + ; make_rewrite (#pattern.ident.Z_mul_split @ #?ℤ @ #?ℤ @ ??{ℤ}) (fun s xx y => (##0, ##0)%Z when Z.eqb xx 0) ; make_rewrite (#pattern.ident.Z_mul_split @ #?ℤ @ ??{ℤ} @ #?ℤ) (fun s y xx => (##0, ##0)%Z when Z.eqb xx 0) ; make_rewrite (#pattern.ident.Z_mul_split @ #?ℤ @ #?ℤ @ ??{ℤ}) (fun s xx y => (y, ##0)%Z when Z.eqb xx 1) @@ -1492,13 +1499,13 @@ In the RHS, the follow notation applies: Definition nbe_dtree' := Eval compute in @compile_rewrites ident var pattern.ident pattern.ident.arg_types pattern.ident.ident_beq 100 nbe_rewrite_rules. Definition arith_dtree' - := Eval compute in @compile_rewrites ident var pattern.ident pattern.ident.arg_types pattern.ident.ident_beq 100 arith_rewrite_rules. + := Eval compute in @compile_rewrites ident var pattern.ident pattern.ident.arg_types pattern.ident.ident_beq 100 (arith_rewrite_rules 0%Z (* dummy val *)). Definition nbe_dtree : decision_tree := Eval compute in invert_Some nbe_dtree'. Definition arith_dtree : decision_tree := Eval compute in invert_Some arith_dtree'. Definition nbe_default_fuel := Eval compute in List.length nbe_rewrite_rules. - Definition arith_default_fuel := Eval compute in List.length arith_rewrite_rules. + Definition arith_default_fuel := Eval compute in List.length (arith_rewrite_rules 0%Z (* dummy val *)). Import PrimitiveHList. (* N.B. The [combine_hlist] call MUST eta-expand @@ -1518,16 +1525,16 @@ In the RHS, the follow notation applies: Definition nbe_pr2_rewrite_rules := Eval hnf in projT2 nbe_split_rewrite_rules. Definition nbe_all_rewrite_rules := combine_hlist (P:=rewrite_ruleTP) nbe_pr1_rewrite_rules nbe_pr2_rewrite_rules. - Definition arith_split_rewrite_rules := Eval cbv [split_list projT1 projT2 arith_rewrite_rules] in split_list arith_rewrite_rules. - Definition arith_pr1_rewrite_rules := Eval hnf in projT1 arith_split_rewrite_rules. - Definition arith_pr2_rewrite_rules := Eval hnf in projT2 arith_split_rewrite_rules. - Definition arith_all_rewrite_rules := combine_hlist (P:=rewrite_ruleTP) arith_pr1_rewrite_rules arith_pr2_rewrite_rules. + Definition arith_split_rewrite_rules max_const_val := Eval cbv [split_list projT1 projT2 arith_rewrite_rules] in split_list (arith_rewrite_rules max_const_val). + Definition arith_pr1_rewrite_rules max_const_val := Eval hnf in projT1 (arith_split_rewrite_rules max_const_val). + Definition arith_pr2_rewrite_rules max_const_val := Eval hnf in projT2 (arith_split_rewrite_rules max_const_val). + Definition arith_all_rewrite_rules max_const_val := combine_hlist (P:=rewrite_ruleTP) (arith_pr1_rewrite_rules max_const_val) (arith_pr2_rewrite_rules max_const_val). Definition nbe_rewrite_head0 do_again {t} (idc : ident t) : value_with_lets t := @assemble_identifier_rewriters nbe_dtree nbe_all_rewrite_rules do_again t idc. - Definition arith_rewrite_head0 do_again {t} (idc : ident t) : value_with_lets t - := @assemble_identifier_rewriters arith_dtree arith_all_rewrite_rules do_again t idc. + Definition arith_rewrite_head0 max_const_val do_again {t} (idc : ident t) : value_with_lets t + := @assemble_identifier_rewriters arith_dtree (arith_all_rewrite_rules max_const_val) do_again t idc. Section fancy. Context (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z). @@ -1907,7 +1914,8 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y) End red_nbe. Section red_arith. - Context {var : type.type base.type -> Type} + Context (max_const_val : Z) + {var : type.type base.type -> Type} (do_again : forall t : base.type, @expr base.type ident (@Compile.value base.type ident var) (type.base t) -> UnderLets.UnderLets base.type ident var (@expr base.type ident var (type.base t))) {t} (idc : ident t). @@ -1923,7 +1931,7 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y) Compile.reflect UnderLets.reify_and_let_binds_base_cps Compile.reify Compile.reify_and_let_binds_cps Compile.value' SubstVarLike.is_var_fst_snd_pair_opp - ] in @arith_rewrite_head0 var do_again t idc. + ] in @arith_rewrite_head0 var max_const_val do_again t idc. (* Finished transaction in 16.593 secs (16.567u,0.s) (successful) *) Time Local Definition arith_rewrite_head2 @@ -1999,8 +2007,8 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y) 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 {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t - := @Compile.Rewrite (@arith_rewrite_head) arith_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. Definition RewriteToFancy (invert_low invert_high : Z (*log2wordmax*) -> Z -> option Z) {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 8a79fc852..9464e270a 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -663,7 +663,7 @@ Module Pipeline. := (*let E := expr.Uncurry E in*) let E := PartialEvaluateWithListInfoFromBounds E arg_bounds in let E := PartialEvaluate E in - let E := RewriteRules.RewriteArith E in + let E := RewriteRules.RewriteArith 0 E in (* Note that DCE evaluates the expr with two different [var] arguments, and so results in a pipeline that is 2x slower unless we pass through a uniformly concrete [var] type @@ -675,11 +675,11 @@ Module Pipeline. let E := FromFlat e in let E := if with_subst01 then Subst01.Subst01 E else E in let E := UnderLets.LetBindReturn E in - let E := RewriteRules.RewriteArith E in (* after inlining, see if any new rewrite redexes are available *) + let E := RewriteRules.RewriteArith 0 E in (* after inlining, see if any new rewrite redexes are available *) dlet_nd e := ToFlat E in let E := FromFlat e in let E := if with_dead_code_elimination then DeadCodeElimination.EliminateDead E else E in - let E := ReassociateSmallConstants.Reassociate (2^8) E in + let E := RewriteRules.RewriteArith (2^8) E in (* reassociate small consts *) let E := match translate_to_fancy with | Some {| invert_low := invert_low ; invert_high := invert_high |} => RewriteRules.RewriteToFancy invert_low invert_high E | None => E diff --git a/src/Experiments/NewPipeline/arith_rewrite_head.out b/src/Experiments/NewPipeline/arith_rewrite_head.out index e71a26c50..99b8053a1 100644 --- a/src/Experiments/NewPipeline/arith_rewrite_head.out +++ b/src/Experiments/NewPipeline/arith_rewrite_head.out @@ -1,5 +1,5 @@ arith_rewrite_head = -match idc in (ident t) return (value' true t) with +match idc in (ident t) return (Compile.value' true t) with | @ident.Literal t v => match t as t0 @@ -48,7 +48,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base A)))) @@ -58,7 +58,7 @@ match idc in (ident t) return (value' true t) with match s as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base A)))) @@ -75,16 +75,18 @@ match idc in (ident t) return (value' true t) with | Some x' => UnderLets.Base (x' v) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.fst) @ (??, ??)) + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.fst) @ (??, ??)) (#(ident.fst)%expr @ x)%expr_pat) end)) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x0) + fun _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x0) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x1) + fun _ : Compile.value' false s1 -> Compile.value' true d1 => + None + end (Compile.reflect x1) | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | @@ -106,7 +108,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base B)))) @@ -116,7 +118,7 @@ match idc in (ident t) return (value' true t) with match s as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base B)))) @@ -133,16 +135,18 @@ match idc in (ident t) return (value' true t) with | Some x' => UnderLets.Base (x' v0) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.snd) @ (??, ??)) + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.snd) @ (??, ??)) (#(ident.snd)%expr @ x)%expr_pat) end)) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x0) + fun _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x0) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x1) + fun _ : Compile.value' false s1 -> Compile.value' true d1 => + None + end (Compile.reflect x1) | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | @@ -358,7 +362,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -378,12 +382,13 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1);; + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x1);; match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -405,8 +410,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1) + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x1) | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None @@ -421,7 +427,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -441,12 +447,13 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1);; + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x1);; match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -468,14 +475,15 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1) + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x1) | @expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x2 => _ <- pattern.ident.invert_bind_args idc0 pattern.ident.Z_opp; match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -492,7 +500,7 @@ match idc in (ident t) return (value' true t) with match s as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -513,14 +521,16 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => - None - end (reflect x1) + fun + _ : Compile.value' false s1 -> + Compile.value' true d1 => None + end (Compile.reflect x1) | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x2) + fun _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x2) | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s0 _ @@ -538,7 +548,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -555,8 +565,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1) + fun _ : Compile.value' false s0 -> Compile.value' true d0 => + None + end (Compile.reflect x1) | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None @@ -568,7 +579,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -585,8 +596,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1) + fun _ : Compile.value' false s0 -> Compile.value' true d0 => + None + end (Compile.reflect x1) | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None @@ -599,6 +611,13 @@ match idc in (ident t) return (value' true t) with (((match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; + match x0 with + | @expr.Ident _ _ _ t0 idc0 => + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; + Some (UnderLets.Base (##(args * args0)%Z)%expr) + | _ => None + end;; (if args =? 0 then Some (UnderLets.Base (##0)%expr) else None) | _ => None end;; @@ -624,7 +643,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -644,8 +663,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1) + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x1) | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None @@ -660,7 +680,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -680,8 +700,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1) + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x1) | _ => None end | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ @@ -723,7 +744,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -740,7 +761,7 @@ match idc in (ident t) return (value' true t) with match s as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -760,14 +781,16 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => - None - end (reflect x1) + fun + _ : Compile.value' false s1 -> + Compile.value' true d1 => None + end (Compile.reflect x1) | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x2) + fun _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x2) | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s0 _ @@ -785,7 +808,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -802,8 +825,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1) + fun _ : Compile.value' false s0 -> Compile.value' true d0 => + None + end (Compile.reflect x1) | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None @@ -820,7 +844,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -837,8 +861,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1) + fun _ : Compile.value' false s0 -> Compile.value' true d0 => + None + end (Compile.reflect x1) | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None @@ -849,6 +874,257 @@ match idc in (ident t) return (value' true t) with args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; (if (args =? 2 ^ Z.log2 args) && negb (args =? 2) then Some (UnderLets.Base (x0 << ##(Z.log2 args))%expr) + else None);; + match x0 with + | @expr.App _ _ _ s _ + (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x2) x1 => + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.Z_mul; + match x2 with + | @expr.Ident _ _ _ t1 idc1 => + args1 <- pattern.ident.invert_bind_args idc1 + pattern.ident.LiteralZ; + match x1 with + | @expr.App _ _ _ s1 _ + (@expr.App _ _ _ s2 _ (@expr.Ident _ _ _ t2 idc2) x4) + x3 => + _ <- pattern.ident.invert_bind_args idc2 + pattern.ident.Z_mul; + match + s2 as t3 + return + (Compile.value' false t3 -> + option + (UnderLets.UnderLets base.type ident var + (defaults.expr (type.base base.type.Z)))) + with + | type.base t3 => + fun v : defaults.expr (type.base t3) => + base.try_make_transport_cps t3 base.type.Z + (fun + a : option + (defaults.expr (type.base t3) -> + defaults.expr (type.base base.type.Z)) + => + match a with + | Some x' => + match + s1 as t4 + return + (Compile.value' false t4 -> + option + (UnderLets.UnderLets base.type ident + var + (defaults.expr + (type.base base.type.Z)))) + with + | type.base t4 => + fun v0 : defaults.expr (type.base t4) + => + base.try_make_transport_cps t4 + base.type.Z + (fun + a0 : option + (defaults.expr + (type.base t4) -> + defaults.expr + (type.base base.type.Z)) + => + match a0 with + | Some x'0 => + if + (Z.abs args <=? + Z.abs max_const_val) && + (Z.abs args1 <=? + Z.abs max_const_val) + then + Some + (UnderLets.Base + (x' v * + (x'0 v0 * + (##args * ##args1)))%expr) + else None + | None => None + end) + | (s3 -> d3)%ptype => + fun + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x3) + | None => None + end) + | (s3 -> d3)%ptype => + fun + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x4) + | @expr.App _ _ _ s1 _ (@expr.App _ _ _ s2 _ ($_)%expr _) + _ | @expr.App _ _ _ s1 _ + (@expr.App _ _ _ s2 _ (@expr.Abs _ _ _ _ _ _) _) _ | + @expr.App _ _ _ s1 _ + (@expr.App _ _ _ s2 _ (_ @ _)%expr_pat _) _ | @expr.App + _ _ _ s1 _ + (@expr.App _ _ _ s2 _ (@expr.LetIn _ _ _ _ _ _ _) _) + _ => None + | @expr.App _ _ _ s1 _ #(_)%expr_pat _ | @expr.App _ _ _ + s1 _ ($_)%expr _ | @expr.App _ _ _ s1 _ + (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s1 _ + (@expr.LetIn _ _ _ _ _ _ _) _ => None + | _ => None + end + | _ => None + end;; + match x1 with + | (@expr.App _ _ _ s2 _ (@expr.Ident _ _ _ t1 idc1) x4 @ x3)%expr_pat => + _ <- pattern.ident.invert_bind_args idc1 + pattern.ident.Z_mul; + match x3 with + | @expr.Ident _ _ _ t2 idc2 => + args2 <- pattern.ident.invert_bind_args idc2 + pattern.ident.LiteralZ; + match + s0 as t3 + return + (Compile.value' false t3 -> + option + (UnderLets.UnderLets base.type ident var + (defaults.expr (type.base base.type.Z)))) + with + | type.base t3 => + fun v : defaults.expr (type.base t3) => + base.try_make_transport_cps t3 base.type.Z + (fun + a : option + (defaults.expr (type.base t3) -> + defaults.expr (type.base base.type.Z)) + => + match a with + | Some x' => + match + s2 as t4 + return + (Compile.value' false t4 -> + option + (UnderLets.UnderLets base.type ident + var + (defaults.expr + (type.base base.type.Z)))) + with + | type.base t4 => + fun v0 : defaults.expr (type.base t4) + => + base.try_make_transport_cps t4 + base.type.Z + (fun + a0 : option + (defaults.expr + (type.base t4) -> + defaults.expr + (type.base base.type.Z)) + => + match a0 with + | Some x'0 => + if + (Z.abs args <=? + Z.abs max_const_val) && + (Z.abs args2 <=? + Z.abs max_const_val) + then + Some + (UnderLets.Base + (x' v * + (x'0 v0 * + (##args * ##args2)))%expr) + else None + | None => None + end) + | (s3 -> d3)%ptype => + fun + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x4) + | None => None + end) + | (s3 -> d3)%ptype => + fun + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x2) + | _ => None + end + | (@expr.App _ _ _ s2 _ ($_)%expr _ @ _)%expr_pat | + (@expr.App _ _ _ s2 _ (@expr.Abs _ _ _ _ _ _) _ @ _)%expr_pat | + (@expr.App _ _ _ s2 _ (_ @ _) _ @ _)%expr_pat | + (@expr.App _ _ _ s2 _ (@expr.LetIn _ _ _ _ _ _ _) _ @ _)%expr_pat => + None + | _ => None + end;; + match + s0 as t2 + return + (Compile.value' false t2 -> + option + (UnderLets.UnderLets base.type ident var + (defaults.expr (type.base base.type.Z)))) + with + | type.base t2 => + fun v : defaults.expr (type.base t2) => + base.try_make_transport_cps t2 base.type.Z + (fun + a : option + (defaults.expr (type.base t2) -> + defaults.expr (type.base base.type.Z)) => + match a with + | Some x' => + match + s as t3 + return + (Compile.value' false t3 -> + option + (UnderLets.UnderLets base.type ident var + (defaults.expr (type.base base.type.Z)))) + with + | type.base t3 => + fun v0 : defaults.expr (type.base t3) => + base.try_make_transport_cps t3 base.type.Z + (fun + a0 : option + (defaults.expr (type.base t3) -> + defaults.expr + (type.base base.type.Z)) => + match a0 with + | Some x'0 => + if Z.abs args <=? Z.abs max_const_val + then + Some + (UnderLets.Base + (x' v * (x'0 v0 * ##args))%expr) + else None + | None => None + end) + | (s1 -> d1)%ptype => + fun + _ : Compile.value' false s1 -> + Compile.value' true d1 => None + end (Compile.reflect x1) + | None => None + end) + | (s1 -> d1)%ptype => + fun _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x2) + | @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 _ _ _ _ _ _ _) _) + _ => None + | @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ + ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | + @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None + | _ => None + end;; + (if Z.abs args <=? Z.abs max_const_val + then Some (UnderLets.Base (x0 * ##args)%expr) else None) | _ => None end);; @@ -868,7 +1144,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -888,8 +1164,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1) + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x1) | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None @@ -911,7 +1188,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -931,12 +1208,13 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1);; + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x1);; match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -957,8 +1235,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1) + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x1) | _ => None end | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ @@ -981,7 +1260,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -1003,12 +1282,13 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1);; + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x1);; match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -1029,8 +1309,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1) + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x1) | _ => None end | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ @@ -1052,7 +1333,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -1069,7 +1350,7 @@ match idc in (ident t) return (value' true t) with match s as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -1089,14 +1370,16 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => - None - end (reflect x1) + fun + _ : Compile.value' false s1 -> + Compile.value' true d1 => None + end (Compile.reflect x1) | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x2) + fun _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x2) | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s0 _ @@ -1114,7 +1397,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -1131,8 +1414,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1) + fun _ : Compile.value' false s0 -> Compile.value' true d0 => + None + end (Compile.reflect x1) | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None @@ -1144,7 +1428,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -1161,8 +1445,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x1) + fun _ : Compile.value' false s0 -> Compile.value' true d0 => + None + end (Compile.reflect x1) | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None @@ -1178,7 +1463,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -1195,8 +1480,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x0) + fun _ : Compile.value' false s0 -> Compile.value' true d0 => + None + end (Compile.reflect x0) | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None @@ -1365,7 +1651,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1393,8 +1679,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x2) + fun _ : Compile.value' false s0 -> Compile.value' true d0 => + None + end (Compile.reflect x2) | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None @@ -1406,7 +1693,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1434,8 +1721,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x2) + fun _ : Compile.value' false s0 -> Compile.value' true d0 => + None + end (Compile.reflect x2) | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None @@ -1524,7 +1812,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1557,12 +1845,13 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x3);; + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x3);; match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1595,8 +1884,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x3) + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x3) | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None @@ -1608,7 +1898,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1641,12 +1931,13 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x3);; + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x3);; match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1679,8 +1970,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x3) + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x3) | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ => None @@ -1769,7 +2061,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1787,7 +2079,7 @@ match idc in (ident t) return (value' true t) with match s0 as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1821,14 +2113,16 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => - None - end (reflect x4) + fun + _ : Compile.value' false s1 -> + Compile.value' true d1 => None + end (Compile.reflect x4) | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x3) + fun _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x3) | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s0 _ @@ -1841,7 +2135,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1859,7 +2153,7 @@ match idc in (ident t) return (value' true t) with match s0 as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1893,14 +2187,16 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => - None - end (reflect x4) + fun + _ : Compile.value' false s1 -> + Compile.value' true d1 => None + end (Compile.reflect x4) | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x3) + fun _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x3) | @expr.App _ _ _ s0 _ ($_)%expr _ | @expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _ | @expr.App _ _ _ s0 _ (_ @ _)%expr_pat _ | @expr.App _ _ _ s0 _ @@ -1914,7 +2210,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1947,8 +2243,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x3) + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x3) | _ => None end;; match x2 with @@ -1958,7 +2255,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1991,8 +2288,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s0 -> d0)%ptype => - fun _ : value' false s0 -> value' true d0 => None - end (reflect x3) + fun _ : Compile.value' false s0 -> Compile.value' true d0 + => None + end (Compile.reflect x3) | _ => None end | @expr.App _ _ _ s _ ($_)%expr _ | @expr.App _ _ _ s _ @@ -2071,7 +2369,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -2089,7 +2387,7 @@ match idc in (ident t) return (value' true t) with match s as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -2115,13 +2413,16 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x0) + fun + _ : Compile.value' false s1 -> + Compile.value' true d1 => None + end (Compile.reflect x0) | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x1) + fun _ : Compile.value' false s1 -> Compile.value' true d1 => + None + end (Compile.reflect x1) | @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 _ _ @@ -2184,4 +2485,4 @@ match idc in (ident t) return (value' true t) with (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) => UnderLets.Base (#(ident.fancy_addm)%expr @ x)%expr_pat end - : value' true t + : Compile.value' true t diff --git a/src/Experiments/NewPipeline/fancy_rewrite_head.out b/src/Experiments/NewPipeline/fancy_rewrite_head.out index 0dfac41db..9b584c48c 100644 --- a/src/Experiments/NewPipeline/fancy_rewrite_head.out +++ b/src/Experiments/NewPipeline/fancy_rewrite_head.out @@ -1,5 +1,5 @@ fancy_rewrite_head = -match idc in (ident t) return (value' true t) with +match idc in (ident t) return (Compile.value' true t) with | @ident.Literal t v => match t as t0 @@ -241,7 +241,7 @@ match idc in (ident t) return (value' true t) with match x0 with | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x2) x1 => - (_ <- pattern.ident.invert_bind_args idc0 pident.Z_land; + (_ <- pattern.ident.invert_bind_args idc0 pattern.ident.Z_land; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 @@ -249,7 +249,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -277,8 +277,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x2) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x2) | _ => None end;; match x2 with @@ -288,7 +290,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -316,12 +318,14 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x1);; + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x1);; match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -349,8 +353,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x1) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x1) | _ => None end;; match x1 with @@ -360,7 +366,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -388,11 +394,13 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x2) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x2) | _ => None end);; - _ <- pattern.ident.invert_bind_args idc0 pident.Z_shiftr; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.Z_shiftr; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 @@ -400,7 +408,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -424,12 +432,14 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x2);; + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x2);; match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -453,8 +463,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x2) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x2) | _ => None end | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @@ -470,7 +482,7 @@ match idc in (ident t) return (value' true t) with end | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x2) x1 => - (_ <- pattern.ident.invert_bind_args idc pident.Z_land; + (_ <- pattern.ident.invert_bind_args idc pattern.ident.Z_land; match x2 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 @@ -482,7 +494,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -510,8 +522,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x1) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x1) | _ => None end | _ => None @@ -527,7 +541,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -555,8 +569,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x2) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x2) | _ => None end | _ => None @@ -572,7 +588,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -600,8 +616,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x1) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x1) | _ => None end | _ => None @@ -617,7 +635,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -645,8 +663,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x2) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x2) | _ => None end | _ => None @@ -658,7 +678,8 @@ match idc in (ident t) return (value' true t) with match x0 with | @expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t1 idc1 @ x4)%expr_pat x3 => - _ <- pattern.ident.invert_bind_args idc1 pident.Z_land; + _ <- pattern.ident.invert_bind_args idc1 + pattern.ident.Z_land; match x4 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 @@ -666,7 +687,7 @@ match idc in (ident t) return (value' true t) with match s as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -684,7 +705,7 @@ match idc in (ident t) return (value' true t) with match s1 as t4 return - (value' false t4 -> + (Compile.value' false t4 -> option (UnderLets.UnderLets base.type ident var @@ -722,14 +743,16 @@ match idc in (ident t) return (value' true t) with end) | (s3 -> d3)%ptype => fun - _ : value' false s3 -> value' true d3 - => None - end (reflect x3) + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x3) | None => None end) | (s3 -> d3)%ptype => - fun _ : value' false s3 -> value' true d3 => None - end (reflect x1) + fun + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x1) | _ => None end | @expr.App _ _ _ s1 _ #(_)%expr_pat _ | @expr.App _ _ _ s1 _ @@ -750,7 +773,8 @@ match idc in (ident t) return (value' true t) with match x0 with | @expr.App _ _ _ s1 _ (@expr.Ident _ _ _ t1 idc1 @ x4)%expr_pat x3 => - _ <- pattern.ident.invert_bind_args idc1 pident.Z_land; + _ <- pattern.ident.invert_bind_args idc1 + pattern.ident.Z_land; match x4 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 @@ -758,7 +782,7 @@ match idc in (ident t) return (value' true t) with match s0 as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -776,7 +800,7 @@ match idc in (ident t) return (value' true t) with match s1 as t4 return - (value' false t4 -> + (Compile.value' false t4 -> option (UnderLets.UnderLets base.type ident var @@ -814,14 +838,16 @@ match idc in (ident t) return (value' true t) with end) | (s3 -> d3)%ptype => fun - _ : value' false s3 -> value' true d3 - => None - end (reflect x3) + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x3) | None => None end) | (s3 -> d3)%ptype => - fun _ : value' false s3 -> value' true d3 => None - end (reflect x2) + fun + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x2) | _ => None end | @expr.App _ _ _ s1 _ #(_)%expr_pat _ | @expr.App _ _ _ s1 _ @@ -841,7 +867,8 @@ match idc in (ident t) return (value' true t) with pattern.ident.LiteralZ; match x0 with | (@expr.App _ _ _ s2 _ (@expr.Ident _ _ _ t1 idc1) x4 @ x3)%expr_pat => - _ <- pattern.ident.invert_bind_args idc1 pident.Z_land; + _ <- pattern.ident.invert_bind_args idc1 + pattern.ident.Z_land; match x3 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 @@ -849,7 +876,7 @@ match idc in (ident t) return (value' true t) with match s as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -867,7 +894,7 @@ match idc in (ident t) return (value' true t) with match s2 as t4 return - (value' false t4 -> + (Compile.value' false t4 -> option (UnderLets.UnderLets base.type ident var @@ -905,14 +932,16 @@ match idc in (ident t) return (value' true t) with end) | (s3 -> d3)%ptype => fun - _ : value' false s3 -> value' true d3 - => None - end (reflect x4) + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x4) | None => None end) | (s3 -> d3)%ptype => - fun _ : value' false s3 -> value' true d3 => None - end (reflect x1) + fun + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x1) | _ => None end | (@expr.App _ _ _ s2 _ ($_)%expr _ @ _)%expr_pat | @@ -930,7 +959,8 @@ match idc in (ident t) return (value' true t) with pattern.ident.LiteralZ; match x0 with | (@expr.App _ _ _ s2 _ (@expr.Ident _ _ _ t1 idc1) x4 @ x3)%expr_pat => - _ <- pattern.ident.invert_bind_args idc1 pident.Z_land; + _ <- pattern.ident.invert_bind_args idc1 + pattern.ident.Z_land; match x3 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 @@ -938,7 +968,7 @@ match idc in (ident t) return (value' true t) with match s0 as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -956,7 +986,7 @@ match idc in (ident t) return (value' true t) with match s2 as t4 return - (value' false t4 -> + (Compile.value' false t4 -> option (UnderLets.UnderLets base.type ident var @@ -994,14 +1024,16 @@ match idc in (ident t) return (value' true t) with end) | (s3 -> d3)%ptype => fun - _ : value' false s3 -> value' true d3 - => None - end (reflect x4) + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x4) | None => None end) | (s3 -> d3)%ptype => - fun _ : value' false s3 -> value' true d3 => None - end (reflect x2) + fun + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x2) | _ => None end | (@expr.App _ _ _ s2 _ ($_)%expr _ @ _)%expr_pat | @@ -1019,7 +1051,8 @@ match idc in (ident t) return (value' true t) with pattern.ident.LiteralZ; match x0 with | (@expr.App _ _ _ s2 _ (@expr.Ident _ _ _ t1 idc1) x4 @ x3)%expr_pat => - _ <- pattern.ident.invert_bind_args idc1 pident.Z_shiftr; + _ <- pattern.ident.invert_bind_args idc1 + pattern.ident.Z_shiftr; match x3 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 @@ -1027,7 +1060,7 @@ match idc in (ident t) return (value' true t) with match s as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -1045,7 +1078,7 @@ match idc in (ident t) return (value' true t) with match s2 as t4 return - (value' false t4 -> + (Compile.value' false t4 -> option (UnderLets.UnderLets base.type ident var @@ -1078,14 +1111,16 @@ match idc in (ident t) return (value' true t) with end) | (s3 -> d3)%ptype => fun - _ : value' false s3 -> value' true d3 - => None - end (reflect x4) + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x4) | None => None end) | (s3 -> d3)%ptype => - fun _ : value' false s3 -> value' true d3 => None - end (reflect x1) + fun + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x1) | _ => None end | (@expr.App _ _ _ s2 _ ($_)%expr _ @ _)%expr_pat | @@ -1103,7 +1138,8 @@ match idc in (ident t) return (value' true t) with pattern.ident.LiteralZ; match x0 with | (@expr.App _ _ _ s2 _ (@expr.Ident _ _ _ t1 idc1) x4 @ x3)%expr_pat => - _ <- pattern.ident.invert_bind_args idc1 pident.Z_shiftr; + _ <- pattern.ident.invert_bind_args idc1 + pattern.ident.Z_shiftr; match x3 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 @@ -1111,7 +1147,7 @@ match idc in (ident t) return (value' true t) with match s0 as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -1129,7 +1165,7 @@ match idc in (ident t) return (value' true t) with match s2 as t4 return - (value' false t4 -> + (Compile.value' false t4 -> option (UnderLets.UnderLets base.type ident var @@ -1162,14 +1198,16 @@ match idc in (ident t) return (value' true t) with end) | (s3 -> d3)%ptype => fun - _ : value' false s3 -> value' true d3 - => None - end (reflect x4) + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x4) | None => None end) | (s3 -> d3)%ptype => - fun _ : value' false s3 -> value' true d3 => None - end (reflect x2) + fun + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x2) | _ => None end | (@expr.App _ _ _ s2 _ ($_)%expr _ @ _)%expr_pat | @@ -1181,7 +1219,7 @@ match idc in (ident t) return (value' true t) with end | _ => None end);; - _ <- pattern.ident.invert_bind_args idc pident.Z_shiftr; + _ <- pattern.ident.invert_bind_args idc pattern.ident.Z_shiftr; match x1 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 @@ -1193,7 +1231,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -1217,12 +1255,14 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x2);; + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x2);; match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -1246,11 +1286,14 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x2) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x2) | @expr.App _ _ _ s1 _ (@expr.App _ _ _ s2 _ (@expr.Ident _ _ _ t1 idc1) x4) x3 => - (_ <- pattern.ident.invert_bind_args idc1 pident.Z_land; + (_ <- pattern.ident.invert_bind_args idc1 + pattern.ident.Z_land; match x4 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 @@ -1258,7 +1301,7 @@ match idc in (ident t) return (value' true t) with match s0 as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -1276,7 +1319,7 @@ match idc in (ident t) return (value' true t) with match s1 as t4 return - (value' false t4 -> + (Compile.value' false t4 -> option (UnderLets.UnderLets base.type ident var @@ -1309,14 +1352,16 @@ match idc in (ident t) return (value' true t) with end) | (s3 -> d3)%ptype => fun - _ : value' false s3 -> value' true d3 - => None - end (reflect x3) + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x3) | None => None end) | (s3 -> d3)%ptype => - fun _ : value' false s3 -> value' true d3 => None - end (reflect x2) + fun + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x2) | _ => None end;; match x3 with @@ -1326,7 +1371,7 @@ match idc in (ident t) return (value' true t) with match s0 as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -1344,7 +1389,7 @@ match idc in (ident t) return (value' true t) with match s2 as t4 return - (value' false t4 -> + (Compile.value' false t4 -> option (UnderLets.UnderLets base.type ident var @@ -1377,17 +1422,20 @@ match idc in (ident t) return (value' true t) with end) | (s3 -> d3)%ptype => fun - _ : value' false s3 -> value' true d3 - => None - end (reflect x4) + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x4) | None => None end) | (s3 -> d3)%ptype => - fun _ : value' false s3 -> value' true d3 => None - end (reflect x2) + fun + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x2) | _ => None end);; - _ <- pattern.ident.invert_bind_args idc1 pident.Z_shiftr; + _ <- pattern.ident.invert_bind_args idc1 + pattern.ident.Z_shiftr; match x3 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 @@ -1395,7 +1443,7 @@ match idc in (ident t) return (value' true t) with match s0 as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -1413,7 +1461,7 @@ match idc in (ident t) return (value' true t) with match s2 as t4 return - (value' false t4 -> + (Compile.value' false t4 -> option (UnderLets.UnderLets base.type ident var @@ -1443,14 +1491,17 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s3 -> d3)%ptype => - fun _ : value' false s3 -> value' true d3 - => None - end (reflect x4) + fun + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x4) | None => None end) | (s3 -> d3)%ptype => - fun _ : value' false s3 -> value' true d3 => None - end (reflect x2) + fun + _ : Compile.value' false s3 -> + Compile.value' true d3 => None + end (Compile.reflect x2) | _ => None end | @expr.App _ _ _ s1 _ (@expr.App _ _ _ s2 _ ($_)%expr _) _ | @@ -1540,7 +1591,7 @@ match idc in (ident t) return (value' true t) with args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x1 with | (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x3 @ x2)%expr_pat => - _ <- pattern.ident.invert_bind_args idc0 pident.Z_shiftl; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.Z_shiftl; match x2 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 @@ -1548,7 +1599,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1573,8 +1624,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x3) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x3) | _ => None end | (@expr.App _ _ _ s0 _ ($_)%expr _ @ _)%expr_pat | @@ -1586,7 +1639,7 @@ match idc in (ident t) return (value' true t) with end;; match x0 with | (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x3 @ x2)%expr_pat => - _ <- pattern.ident.invert_bind_args idc0 pident.Z_shiftl; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.Z_shiftl; match x2 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 @@ -1594,7 +1647,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1619,8 +1672,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x3) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x3) | _ => None end | (@expr.App _ _ _ s0 _ ($_)%expr _ @ _)%expr_pat | @@ -1632,7 +1687,7 @@ match idc in (ident t) return (value' true t) with end;; match x1 with | (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x3 @ x2)%expr_pat => - _ <- pattern.ident.invert_bind_args idc0 pident.Z_shiftr; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.Z_shiftr; match x2 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 @@ -1640,7 +1695,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1665,8 +1720,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x3) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x3) | _ => None end | (@expr.App _ _ _ s0 _ ($_)%expr _ @ _)%expr_pat | @@ -1678,7 +1735,7 @@ match idc in (ident t) return (value' true t) with end;; match x0 with | (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x3 @ x2)%expr_pat => - _ <- pattern.ident.invert_bind_args idc0 pident.Z_shiftr; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.Z_shiftr; match x2 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 @@ -1686,7 +1743,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1711,8 +1768,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x3) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x3) | _ => None end | (@expr.App _ _ _ s0 _ ($_)%expr _ @ _)%expr_pat | @@ -1742,7 +1801,7 @@ match idc in (ident t) return (value' true t) with args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x2 with | (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x4 @ x3)%expr_pat => - _ <- pattern.ident.invert_bind_args idc0 pident.Z_shiftl; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.Z_shiftl; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 @@ -1750,7 +1809,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1775,8 +1834,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x4) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x4) | _ => None end | (@expr.App _ _ _ s0 _ ($_)%expr _ @ _)%expr_pat | @@ -1788,7 +1849,7 @@ match idc in (ident t) return (value' true t) with end;; match x1 with | (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x4 @ x3)%expr_pat => - _ <- pattern.ident.invert_bind_args idc0 pident.Z_shiftl; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.Z_shiftl; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 @@ -1796,7 +1857,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1821,8 +1882,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x4) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x4) | _ => None end | (@expr.App _ _ _ s0 _ ($_)%expr _ @ _)%expr_pat | @@ -1834,7 +1897,7 @@ match idc in (ident t) return (value' true t) with end;; match x2 with | (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x4 @ x3)%expr_pat => - _ <- pattern.ident.invert_bind_args idc0 pident.Z_shiftr; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.Z_shiftr; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 @@ -1842,7 +1905,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1867,8 +1930,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x4) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x4) | _ => None end | (@expr.App _ _ _ s0 _ ($_)%expr _ @ _)%expr_pat | @@ -1880,7 +1945,7 @@ match idc in (ident t) return (value' true t) with end;; match x1 with | (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x4 @ x3)%expr_pat => - _ <- pattern.ident.invert_bind_args idc0 pident.Z_shiftr; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.Z_shiftr; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 @@ -1888,7 +1953,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1913,8 +1978,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x4) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x4) | _ => None end | (@expr.App _ _ _ s0 _ ($_)%expr _ @ _)%expr_pat | @@ -1942,7 +2009,8 @@ match idc in (ident t) return (value' true t) with args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x1 with | (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x3 @ x2)%expr_pat => - (_ <- pattern.ident.invert_bind_args idc0 pident.Z_shiftl; + (_ <- pattern.ident.invert_bind_args idc0 + pattern.ident.Z_shiftl; match x2 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 @@ -1950,7 +2018,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1975,11 +2043,13 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x3) + fun + _ : Compile.value' false s1 -> + Compile.value' true d1 => None + end (Compile.reflect x3) | _ => None end);; - _ <- pattern.ident.invert_bind_args idc0 pident.Z_shiftr; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.Z_shiftr; match x2 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 @@ -1987,7 +2057,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -2012,8 +2082,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x3) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x3) | _ => None end | (@expr.App _ _ _ s0 _ ($_)%expr _ @ _)%expr_pat | @@ -2040,7 +2112,8 @@ match idc in (ident t) return (value' true t) with args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x2 with | (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t0 idc0) x4 @ x3)%expr_pat => - (_ <- pattern.ident.invert_bind_args idc0 pident.Z_shiftl; + (_ <- pattern.ident.invert_bind_args idc0 + pattern.ident.Z_shiftl; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 @@ -2048,7 +2121,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -2073,11 +2146,13 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x4) + fun + _ : Compile.value' false s1 -> + Compile.value' true d1 => None + end (Compile.reflect x4) | _ => None end);; - _ <- pattern.ident.invert_bind_args idc0 pident.Z_shiftr; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.Z_shiftr; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 @@ -2085,7 +2160,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -2110,8 +2185,10 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x4) + fun + _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x4) | _ => None end | (@expr.App _ _ _ s0 _ ($_)%expr _ @ _)%expr_pat | @@ -2137,7 +2214,7 @@ match idc in (ident t) return (value' true t) with (((match x with | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Ident _ _ _ t idc) x3) x2 => - (_ <- pattern.ident.invert_bind_args idc pident.Z_cc_m; + (_ <- pattern.ident.invert_bind_args idc pattern.ident.Z_cc_m; match x3 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 @@ -2145,7 +2222,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -2169,11 +2246,12 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x2) + fun _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x2) | _ => None end);; - _ <- pattern.ident.invert_bind_args idc pident.Z_land; + _ <- pattern.ident.invert_bind_args idc pattern.ident.Z_land; match x3 with | @expr.Ident _ _ _ t0 idc0 => args0 <- pattern.ident.invert_bind_args idc0 @@ -2181,7 +2259,7 @@ match idc in (ident t) return (value' true t) with match s as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -2204,8 +2282,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x2) + fun _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x2) | _ => None end;; match x2 with @@ -2215,7 +2294,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.Z)))) @@ -2238,8 +2317,9 @@ match idc in (ident t) return (value' true t) with | None => None end) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x3) + fun _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x3) | _ => None end | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App @@ -2340,4 +2420,4 @@ match idc in (ident t) return (value' true t) with (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) => UnderLets.Base (#(ident.fancy_addm)%expr @ x)%expr_pat end - : value' true t + : Compile.value' true t diff --git a/src/Experiments/NewPipeline/nbe_rewrite_head.out b/src/Experiments/NewPipeline/nbe_rewrite_head.out index e5808c478..6d0dafb7d 100644 --- a/src/Experiments/NewPipeline/nbe_rewrite_head.out +++ b/src/Experiments/NewPipeline/nbe_rewrite_head.out @@ -1,5 +1,5 @@ nbe_rewrite_head = -match idc in (ident t) return (value' true t) with +match idc in (ident t) return (Compile.value' true t) with | @ident.Literal t v => match t as t0 @@ -17,7 +17,7 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralNat; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; Some (UnderLets.Base (##(Nat.succ args))%expr) | _ => None end;; @@ -27,7 +27,7 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralNat; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; Some (UnderLets.Base (##(Nat.pred args))%expr) | _ => None end;; @@ -37,10 +37,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralNat; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralNat; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralNat; Some (UnderLets.Base (##(Nat.max args args0))%expr) | _ => None end @@ -52,10 +53,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralNat; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralNat; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralNat; Some (UnderLets.Base (##(args * args0)%nat)%expr) | _ => None end @@ -67,10 +69,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralNat; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralNat; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralNat; Some (UnderLets.Base (##(args + args0)%nat)%expr) | _ => None end @@ -82,10 +85,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralNat; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralNat; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralNat; Some (UnderLets.Base (##(args - args0)%nat)%expr) | _ => None end @@ -110,7 +114,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base A)))) @@ -120,7 +124,7 @@ match idc in (ident t) return (value' true t) with match s as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base A)))) @@ -137,16 +141,18 @@ match idc in (ident t) return (value' true t) with | Some x' => UnderLets.Base (x' v) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.fst) @ (??, ??)) + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.fst) @ (??, ??)) (#(ident.fst)%expr @ x)%expr_pat) end)) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x0) + fun _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x0) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x1) + fun _ : Compile.value' false s1 -> Compile.value' true d1 => + None + end (Compile.reflect x1) | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | @@ -168,7 +174,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base B)))) @@ -178,7 +184,7 @@ match idc in (ident t) return (value' true t) with match s as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base B)))) @@ -195,16 +201,18 @@ match idc in (ident t) return (value' true t) with | Some x' => UnderLets.Base (x' v0) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.snd) @ (??, ??)) + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.snd) @ (??, ??)) (#(ident.snd)%expr @ x)%expr_pat) end)) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x0) + fun _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x0) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x1) + fun _ : Compile.value' false s1 -> Compile.value' true d1 => + None + end (Compile.reflect x1) | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | @@ -231,7 +239,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base T)))) @@ -241,21 +249,21 @@ match idc in (ident t) return (value' true t) with match s as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base T)))) with | type.base t3 => fun v0 : defaults.expr (type.base t3) => - castbe v + Compile.castbe v (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base T)))) (fun x3 : option (defaults.expr (type.base A)) => (x4 <- x3; Some - (castbe v0 + (Compile.castbe v0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base T)))) @@ -297,8 +305,8 @@ match idc in (ident t) return (value' true t) with unwrap)) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.prod_rect) @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.prod_rect) @ ??{?? -> ?? -> ??} @ (??, ??)) (#(ident.prod_rect)%expr @ @@ -310,11 +318,13 @@ match idc in (ident t) return (value' true t) with None)));;; None) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x1) + fun _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x1) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x2) + fun _ : Compile.value' false s1 -> Compile.value' true d1 => + None + end (Compile.reflect x2) | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | @@ -373,9 +383,9 @@ match idc in (ident t) return (value' true t) with unwrap)) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.bool_rect) @ ??{() -> ??} @ ??{() -> ??} @ - #(pattern.ident.LiteralBool)) + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.bool_rect) @ ??{() -> ??} @ + ??{() -> ??} @ #(pattern.ident.LiteralBool)) (#(ident.bool_rect)%expr @ (λ x2 : var (type.base base.type.unit), UnderLets.to_expr (x ($x2)))%expr @ @@ -404,7 +414,7 @@ match idc in (ident t) return (value' true t) with ((match x1 with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; - castv x0 + Compile.castv x0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base P)))) @@ -451,8 +461,8 @@ match idc in (ident t) return (value' true t) with unwrap)) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.nat_rect) @ ??{() -> ??} @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.nat_rect) @ ??{() -> ??} @ ??{type.base base.type.nat -> ?? -> ??} @ #(pattern.ident.LiteralNat)) (#(ident.nat_rect)%expr @ @@ -490,7 +500,7 @@ match idc in (ident t) return (value' true t) with (match x1 with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; - castv x0 + Compile.castv x0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base Q)))) @@ -505,7 +515,7 @@ match idc in (ident t) return (value' true t) with (defaults.expr (type.base Q))) => (S_case0 <- S_case; Some - (castbe x2 + (Compile.castbe x2 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base Q)))) @@ -556,8 +566,8 @@ match idc in (ident t) return (value' true t) with unwrap)) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.nat_rect_arrow) @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.nat_rect_arrow) @ ??{?? -> ??} @ ??{type.base base.type.nat -> (?? -> ??) -> ?? -> ??} @ @@ -606,7 +616,7 @@ match idc in (ident t) return (value' true t) with UnderLets.UnderLets base.type ident var (defaults.expr (type.base P))) (x1 : defaults.expr (type.base (base.type.list A))) => - ((castv x0 + ((Compile.castv x0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base P)))) @@ -668,8 +678,8 @@ match idc in (ident t) return (value' true t) with unwrap)) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.list_rect) @ ??{() -> ??} @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.list_rect) @ ??{() -> ??} @ ??{?? -> ?? -> ?? -> ??} @ ??{type.base (pattern.base.type.list ??)}) (#(ident.list_rect)%expr @ @@ -732,8 +742,8 @@ match idc in (ident t) return (value' true t) with unwrap)) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.list_case) @ ??{() -> ??} @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.list_case) @ ??{() -> ??} @ ??{?? -> ?? -> ??} @ []) (#(ident.list_case)%expr @ (λ x2 : var (type.base base.type.unit), @@ -750,7 +760,7 @@ match idc in (ident t) return (value' true t) with match s0 as t2 return - (value' false t2 -> + (Compile.value' false t2 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base P)))) @@ -760,21 +770,21 @@ match idc in (ident t) return (value' true t) with match s as t3 return - (value' false t3 -> + (Compile.value' false t3 -> option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base P)))) with | type.base t3 => fun v0 : defaults.expr (type.base t3) => - castbe v + Compile.castbe v (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base P)))) (fun x4 : option (defaults.expr (type.base A)) => (x5 <- x4; Some - (castbe v0 + (Compile.castbe v0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base P)))) @@ -819,8 +829,8 @@ match idc in (ident t) return (value' true t) with unwrap)) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.list_case) @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.list_case) @ ??{() -> ??} @ ??{?? -> ?? -> ??} @ (?? :: ??)) @@ -840,11 +850,13 @@ match idc in (ident t) return (value' true t) with None)));;; None) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x2) + fun _ : Compile.value' false s1 -> Compile.value' true d1 + => None + end (Compile.reflect x2) | (s1 -> d1)%ptype => - fun _ : value' false s1 -> value' true d1 => None - end (reflect x3) + fun _ : Compile.value' false s1 -> Compile.value' true d1 => + None + end (Compile.reflect x3) | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ | @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ | @@ -874,10 +886,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralNat; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralNat; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralNat; Some (UnderLets.Base (fold_right @@ -914,8 +927,8 @@ match idc in (ident t) return (value' true t) with UnderLets.Base (x' (reify_list (firstn args xs0))) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.List_firstn) @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.List_firstn) @ #(pattern.ident.LiteralNat) @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_firstn)%expr @ x @ x0)%expr_pat) @@ -947,8 +960,8 @@ match idc in (ident t) return (value' true t) with UnderLets.Base (x' (reify_list (skipn args xs0))) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.List_skipn) @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.List_skipn) @ #(pattern.ident.LiteralNat) @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_skipn)%expr @ x @ x0)%expr_pat) @@ -974,8 +987,8 @@ match idc in (ident t) return (value' true t) with | Some x' => UnderLets.Base (x' (reify_list (repeat x args))) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.List_repeat) @ ?? @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.List_repeat) @ ?? @ #(pattern.ident.LiteralNat)) (#(ident.List_repeat)%expr @ x @ x0)%expr_pat) end)) @@ -1028,8 +1041,8 @@ match idc in (ident t) return (value' true t) with (combine xs0 ys0)))) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.List_combine) @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.List_combine) @ ??{type.base (pattern.base.type.list ??)} @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_combine)%expr @ x @ x0)%expr_pat) @@ -1043,7 +1056,7 @@ match idc in (ident t) return (value' true t) with UnderLets.UnderLets base.type ident var (defaults.expr (type.base B))) (x0 : defaults.expr (type.base (base.type.list A))) => - ((castbe x0 + ((Compile.castbe x0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list B))))) @@ -1109,8 +1122,8 @@ match idc in (ident t) return (value' true t) with unwrap)) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.List_map) @ ??{?? -> ??} @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.List_map) @ ??{?? -> ??} @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_map)%expr @ (λ x1 : var (type.base A), @@ -1125,7 +1138,7 @@ match idc in (ident t) return (value' true t) with UnderLets.to_expr (x ($x1)))%expr @ x0)%expr_pat)%option | @ident.List_app A => fun x x0 : defaults.expr (type.base (base.type.list A)) => - ((castbe x + ((Compile.castbe x (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list A))))) @@ -1190,7 +1203,7 @@ match idc in (ident t) return (value' true t) with unwrap)) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE + (Compile.ERROR_BAD_REWRITE_RULE (??{type.base (pattern.base.type.list ??)} ++ ??{type.base (pattern.base.type.list ??)}) (x ++ x0)) @@ -1215,8 +1228,8 @@ match idc in (ident t) return (value' true t) with | Some x' => UnderLets.Base (x' (reify_list (rev xs0))) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.List_rev) @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.List_rev) @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_rev)%expr @ x)%expr_pat) end))));;; @@ -1229,7 +1242,7 @@ match idc in (ident t) return (value' true t) with UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list B)))) (x0 : defaults.expr (type.base (base.type.list A))) => - ((castbe x0 + ((Compile.castbe x0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list B))))) @@ -1295,8 +1308,8 @@ match idc in (ident t) return (value' true t) with | Some x' => UnderLets.Base (x' fv0) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.List_flat_map) @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.List_flat_map) @ ??{?? -> type.base (pattern.base.type.list ??)} @ ??{type.base (pattern.base.type.list ??)}) @@ -1317,7 +1330,7 @@ match idc in (ident t) return (value' true t) with UnderLets.UnderLets base.type ident var (defaults.expr (type.base base.type.bool))) (x0 : defaults.expr (type.base (base.type.list A))) => - ((castbe x0 + ((Compile.castbe x0 (option (UnderLets.UnderLets base.type ident var (defaults.expr @@ -1405,8 +1418,8 @@ match idc in (ident t) return (value' true t) with | Some x' => UnderLets.Base (x' fv0) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.List_partition) @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.List_partition) @ ??{?? -> type.base base.type.bool} @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_partition)%expr @ @@ -1428,7 +1441,7 @@ match idc in (ident t) return (value' true t) with (defaults.expr (type.base A))) (x0 : defaults.expr (type.base A)) (x1 : defaults.expr (type.base (base.type.list B))) => - ((castv x + ((Compile.castv x (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base A)))) @@ -1488,8 +1501,8 @@ match idc in (ident t) return (value' true t) with unwrap)) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.List_fold_right) @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.List_fold_right) @ ??{?? -> ?? -> ??} @ ?? @ ??{type.base (pattern.base.type.list ??)}) (#(ident.List_fold_right)%expr @ @@ -1516,7 +1529,7 @@ match idc in (ident t) return (value' true t) with (match x with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; - castv x0 + Compile.castv x0 (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base (base.type.list T))))) @@ -1574,8 +1587,8 @@ match idc in (ident t) return (value' true t) with unwrap)) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.List_update_nth) @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.List_update_nth) @ #(pattern.ident.LiteralNat) @ ??{?? -> ??} @ ??{type.base @@ -1600,7 +1613,7 @@ match idc in (ident t) return (value' true t) with ((match x1 with | @expr.Ident _ _ _ t idc => args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; - castbe x + Compile.castbe x (option (UnderLets.UnderLets base.type ident var (defaults.expr (type.base T)))) @@ -1623,8 +1636,9 @@ match idc in (ident t) return (value' true t) with (x' (nth_default default0 ls0 args)) | None => UnderLets.Base - (ERROR_BAD_REWRITE_RULE - (#(pident.List_nth_default) @ ?? @ + (Compile.ERROR_BAD_REWRITE_RULE + (#(pattern.ident.List_nth_default) @ + ?? @ ??{type.base (pattern.base.type.list ??)} @ #(pattern.ident.LiteralNat)) @@ -1641,10 +1655,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; Some (UnderLets.Base (##(args + args0)%Z)%expr) | _ => None end @@ -1656,10 +1671,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; Some (UnderLets.Base (##(args * args0)%Z)%expr) | _ => None end @@ -1671,10 +1687,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; Some (UnderLets.Base (##(args ^ args0))%expr) | _ => None end @@ -1686,10 +1703,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; Some (UnderLets.Base (##(args - args0)%Z)%expr) | _ => None end @@ -1701,7 +1719,7 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; Some (UnderLets.Base (##(- args)%Z)%expr) | _ => None end;; @@ -1711,10 +1729,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; Some (UnderLets.Base (##(args / args0)%Z)%expr) | _ => None end @@ -1726,10 +1745,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; Some (UnderLets.Base (##(args mod args0)%Z)%expr) | _ => None end @@ -1741,7 +1761,7 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; Some (UnderLets.Base (##(Z.log2 args))%expr) | _ => None end;; @@ -1751,7 +1771,7 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; Some (UnderLets.Base (##(Z.log2_up args))%expr) | _ => None end;; @@ -1761,10 +1781,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; Some (UnderLets.Base (##(args =? args0))%expr) | _ => None end @@ -1776,10 +1797,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; Some (UnderLets.Base (##(args <=? args0))%expr) | _ => None end @@ -1791,10 +1813,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; Some (UnderLets.Base (##(args >=? args0))%expr) | _ => None end @@ -1806,7 +1829,7 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base base.type.nat) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralNat; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralNat; Some (UnderLets.Base (##(Z.of_nat args))%expr) | _ => None end;; @@ -1816,7 +1839,7 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; Some (UnderLets.Base (##(Z.to_nat args))%expr) | _ => None end;; @@ -1826,10 +1849,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; Some (UnderLets.Base (##(Z.shiftr args args0))%expr) | _ => None end @@ -1841,10 +1865,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; Some (UnderLets.Base (##(Z.shiftl args args0))%expr) | _ => None end @@ -1856,10 +1881,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; Some (UnderLets.Base (##(Z.land args args0))%expr) | _ => None end @@ -1871,10 +1897,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; Some (UnderLets.Base (##(Z.lor args args0))%expr) | _ => None end @@ -1886,7 +1913,7 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; Some (UnderLets.Base (##(Definitions.Z.bneg args))%expr) | _ => None end;; @@ -1896,10 +1923,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; Some (UnderLets.Base (##(Definitions.Z.lnot_modulo args args0))%expr) @@ -1913,14 +1941,15 @@ match idc in (ident t) return (value' true t) with fun x x0 x1 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (let @@ -1938,14 +1967,15 @@ match idc in (ident t) return (value' true t) with fun x x0 x1 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (let @@ -1964,14 +1994,15 @@ match idc in (ident t) return (value' true t) with fun x x0 x1 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (##(Definitions.Z.add_with_carry args args0 args1))%expr) @@ -1987,18 +2018,19 @@ match idc in (ident t) return (value' true t) with fun x x0 x1 x2 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (let @@ -2021,14 +2053,15 @@ match idc in (ident t) return (value' true t) with fun x x0 x1 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (let @@ -2047,18 +2080,19 @@ match idc in (ident t) return (value' true t) with fun x x0 x1 x2 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (let @@ -2081,14 +2115,15 @@ match idc in (ident t) return (value' true t) with fun x x0 x1 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (##(Definitions.Z.zselect args args0 args1))%expr) @@ -2104,14 +2139,15 @@ match idc in (ident t) return (value' true t) with fun x x0 x1 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (##(Definitions.Z.add_modulo args args0 args1))%expr) @@ -2127,18 +2163,19 @@ match idc in (ident t) return (value' true t) with fun x x0 x1 x2 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (##(Definitions.Z.rshi args args0 args1 args2))%expr) @@ -2156,10 +2193,11 @@ match idc in (ident t) return (value' true t) with fun x x0 : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; Some (UnderLets.Base (##(Definitions.Z.cc_m args args0))%expr) | _ => None end @@ -2171,7 +2209,7 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base base.type.Z) => ((match x with | @expr.Ident _ _ _ t idc => - args <- pattern.ident.invert_bind_args idc pident.LiteralZ; + args <- pattern.ident.invert_bind_args idc pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.cast ident.cast_outside_of_range range args))%expr) @@ -2183,14 +2221,15 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => - _ <- pattern.ident.invert_bind_args idc pident.pair; + _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (let @@ -2213,14 +2252,15 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => - _ <- pattern.ident.invert_bind_args idc pident.pair; + _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (let @@ -2245,22 +2285,22 @@ match idc in (ident t) return (value' true t) with (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => - _ <- pattern.ident.invert_bind_args idc pident.pair; + _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | (@expr.Ident _ _ _ t0 idc0 @ x3 @ x2)%expr_pat => - _ <- pattern.ident.invert_bind_args idc0 pident.pair; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.pair; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 - pident.LiteralZ; + pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t3 idc3 => args3 <- pattern.ident.invert_bind_args idc3 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (let @@ -2287,14 +2327,15 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => - _ <- pattern.ident.invert_bind_args idc pident.pair; + _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (let @@ -2319,22 +2360,22 @@ match idc in (ident t) return (value' true t) with (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => - _ <- pattern.ident.invert_bind_args idc pident.pair; + _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | (@expr.Ident _ _ _ t0 idc0 @ x3 @ x2)%expr_pat => - _ <- pattern.ident.invert_bind_args idc0 pident.pair; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.pair; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 - pident.LiteralZ; + pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t3 idc3 => args3 <- pattern.ident.invert_bind_args idc3 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (let @@ -2361,14 +2402,15 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => - _ <- pattern.ident.invert_bind_args idc pident.pair; + _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp @@ -2388,14 +2430,15 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => - _ <- pattern.ident.invert_bind_args idc pident.pair; + _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp @@ -2415,14 +2458,15 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => - _ <- pattern.ident.invert_bind_args idc pident.pair; + _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp @@ -2442,14 +2486,15 @@ match idc in (ident t) return (value' true t) with fun x : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => - _ <- pattern.ident.invert_bind_args idc pident.pair; + _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp @@ -2469,14 +2514,15 @@ match idc in (ident t) return (value' true t) with fun x0 : defaults.expr (type.base (base.type.Z * base.type.Z)%etype) => ((match x0 with | (@expr.Ident _ _ _ t idc @ x2 @ x1)%expr_pat => - _ <- pattern.ident.invert_bind_args idc pident.pair; + _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x2 with | @expr.Ident _ _ _ t0 idc0 => - args0 <- pattern.ident.invert_bind_args idc0 pident.LiteralZ; + args0 <- pattern.ident.invert_bind_args idc0 + pattern.ident.LiteralZ; match x1 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp @@ -2498,22 +2544,22 @@ match idc in (ident t) return (value' true t) with (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => - _ <- pattern.ident.invert_bind_args idc pident.pair; + _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | (@expr.Ident _ _ _ t0 idc0 @ x3 @ x2)%expr_pat => - _ <- pattern.ident.invert_bind_args idc0 pident.pair; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.pair; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 - pident.LiteralZ; + pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t3 idc3 => args3 <- pattern.ident.invert_bind_args idc3 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp @@ -2538,22 +2584,22 @@ match idc in (ident t) return (value' true t) with (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => - _ <- pattern.ident.invert_bind_args idc pident.pair; + _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | (@expr.Ident _ _ _ t0 idc0 @ x3 @ x2)%expr_pat => - _ <- pattern.ident.invert_bind_args idc0 pident.pair; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.pair; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 - pident.LiteralZ; + pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t3 idc3 => args3 <- pattern.ident.invert_bind_args idc3 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp @@ -2579,22 +2625,22 @@ match idc in (ident t) return (value' true t) with (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => - _ <- pattern.ident.invert_bind_args idc pident.pair; + _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | (@expr.Ident _ _ _ t0 idc0 @ x3 @ x2)%expr_pat => - _ <- pattern.ident.invert_bind_args idc0 pident.pair; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.pair; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 - pident.LiteralZ; + pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t3 idc3 => args3 <- pattern.ident.invert_bind_args idc3 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp @@ -2619,22 +2665,22 @@ match idc in (ident t) return (value' true t) with (type.base (base.type.Z * base.type.Z * base.type.Z)%etype) => ((match x with | (@expr.Ident _ _ _ t idc @ x1 @ x0)%expr_pat => - _ <- pattern.ident.invert_bind_args idc pident.pair; + _ <- pattern.ident.invert_bind_args idc pattern.ident.pair; match x1 with | (@expr.Ident _ _ _ t0 idc0 @ x3 @ x2)%expr_pat => - _ <- pattern.ident.invert_bind_args idc0 pident.pair; + _ <- pattern.ident.invert_bind_args idc0 pattern.ident.pair; match x3 with | @expr.Ident _ _ _ t1 idc1 => args1 <- pattern.ident.invert_bind_args idc1 - pident.LiteralZ; + pattern.ident.LiteralZ; match x2 with | @expr.Ident _ _ _ t2 idc2 => args2 <- pattern.ident.invert_bind_args idc2 - pident.LiteralZ; + pattern.ident.LiteralZ; match x0 with | @expr.Ident _ _ _ t3 idc3 => args3 <- pattern.ident.invert_bind_args idc3 - pident.LiteralZ; + pattern.ident.LiteralZ; Some (UnderLets.Base (##(ident.fancy.interp @@ -2654,4 +2700,4 @@ match idc in (ident t) return (value' true t) with None);;; UnderLets.Base (#(ident.fancy_addm)%expr @ x)%expr_pat)%option end - : value' true t + : Compile.value' true t |