aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2018-07-26 19:28:52 -0400
committerGravatar Jason Gross <jagro@google.com>2018-07-26 19:28:52 -0400
commitf2f418416535d91d9e7c7f6f083f898737adb9ee (patch)
treebe26bff1fde4be4b106dbe7c9a194815153c758c
parent91b0b095de58548e927c28550db376692b692c5b (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
-rw-r--r--src/Experiments/NewPipeline/CompilersTestCases.v22
-rw-r--r--src/Experiments/NewPipeline/MiscCompilerPasses.v64
-rw-r--r--src/Experiments/NewPipeline/README.md3
-rw-r--r--src/Experiments/NewPipeline/Rewriter.v34
-rw-r--r--src/Experiments/NewPipeline/Toplevel1.v6
-rw-r--r--src/Experiments/NewPipeline/arith_rewrite_head.out575
-rw-r--r--src/Experiments/NewPipeline/fancy_rewrite_head.out424
-rw-r--r--src/Experiments/NewPipeline/nbe_rewrite_head.out478
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 09:39:35 +0000