aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Experiments/NewPipeline/AbstractInterpretation.v2
-rw-r--r--src/Experiments/NewPipeline/CStringification.v4
-rw-r--r--src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v30
-rw-r--r--src/Experiments/NewPipeline/Language.v22
-rw-r--r--src/Experiments/NewPipeline/Rewriter.v4
-rw-r--r--src/Experiments/NewPipeline/fancy_rewrite_head.out4
-rw-r--r--src/Experiments/NewPipeline/rewrite_head.out28
7 files changed, 47 insertions, 47 deletions
diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v
index 55aa92ddc..3f905a869 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretation.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretation.v
@@ -480,7 +480,7 @@ Module Compilers.
| ident.pair A B => pair
| ident.fst A B => fst
| ident.snd A B => snd
- | ident.pair_rect A B P => fun f '(a, b) => f a b
+ | ident.prod_rect A B P => fun f '(a, b) => f a b
| ident.List_map _ _
=> fun f ls => ls <- ls; Some (List.map f ls)
| ident.List_app _
diff --git a/src/Experiments/NewPipeline/CStringification.v b/src/Experiments/NewPipeline/CStringification.v
index 6072d8ce6..57a2215cc 100644
--- a/src/Experiments/NewPipeline/CStringification.v
+++ b/src/Experiments/NewPipeline/CStringification.v
@@ -174,7 +174,7 @@ Module Compilers.
| ident.pair A B => "(,)"
| ident.fst A B => "fst"
| ident.snd A B => "snd"
- | ident.pair_rect A B T => "pair_rect"
+ | ident.prod_rect A B T => "prod_rect"
| ident.bool_rect T => "bool_rect"
| ident.nat_rect P => "nat_rect"
| ident.list_rect A P => "list_rect"
@@ -876,7 +876,7 @@ Module Compilers.
| ident.Nat_mul
| ident.Nat_add
| ident.Nat_sub
- | ident.pair_rect _ _ _
+ | ident.prod_rect _ _ _
| ident.bool_rect _
| ident.nat_rect _
| ident.list_rect _ _
diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
index 589b5ad26..3b376ae4e 100644
--- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
+++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
@@ -82,7 +82,7 @@ print_ident = r"""Inductive ident : defaults.type -> Set :=
ident
((fun x : base.type => type.base x) (A * B)%etype ->
(fun x : base.type => type.base x) B)
- | pair_rect : forall A B T : base.type,
+ | prod_rect : forall A B T : base.type,
ident
(((fun x : base.type => type.base x) A ->
(fun x : base.type => type.base x) B ->
@@ -567,7 +567,7 @@ show_match_ident = r"""match # with
| ident.pair A B =>
| ident.fst A B =>
| ident.snd A B =>
- | ident.pair_rect A B T =>
+ | ident.prod_rect A B T =>
| ident.bool_rect T =>
| ident.nat_rect P =>
| ident.list_rect A P =>
@@ -856,7 +856,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| pair
| fst
| snd
- | pair_rect
+ | prod_rect
| bool_rect
| nat_rect
| list_rect
@@ -936,7 +936,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| pair, pair
| fst, fst
| snd, snd
- | pair_rect, pair_rect
+ | prod_rect, prod_rect
| bool_rect, bool_rect
| nat_rect, nat_rect
| list_rect, list_rect
@@ -1014,7 +1014,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| pair, _
| fst, _
| snd, _
- | pair_rect, _
+ | prod_rect, _
| bool_rect, _
| nat_rect, _
| list_rect, _
@@ -1098,7 +1098,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| Compilers.ident.pair A B => f _ (@Compilers.ident.pair A B)
| Compilers.ident.fst A B => f _ (@Compilers.ident.fst A B)
| Compilers.ident.snd A B => f _ (@Compilers.ident.snd A B)
- | Compilers.ident.pair_rect A B T => f _ (@Compilers.ident.pair_rect A B T)
+ | Compilers.ident.prod_rect A B T => f _ (@Compilers.ident.prod_rect A B T)
| Compilers.ident.bool_rect T => f _ (@Compilers.ident.bool_rect T)
| Compilers.ident.nat_rect P => f _ (@Compilers.ident.nat_rect P)
| Compilers.ident.list_rect A P => f _ (@Compilers.ident.list_rect A P)
@@ -1179,7 +1179,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| Compilers.ident.pair A B => pair
| Compilers.ident.fst A B => fst
| Compilers.ident.snd A B => snd
- | Compilers.ident.pair_rect A B T => pair_rect
+ | Compilers.ident.prod_rect A B T => prod_rect
| Compilers.ident.bool_rect T => bool_rect
| Compilers.ident.nat_rect P => nat_rect
| Compilers.ident.list_rect A P => list_rect
@@ -1260,7 +1260,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| pair => None
| fst => None
| snd => None
- | pair_rect => None
+ | prod_rect => None
| bool_rect => None
| nat_rect => None
| list_rect => None
@@ -1341,7 +1341,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| pair => base.type * base.type
| fst => base.type * base.type
| snd => base.type * base.type
- | pair_rect => base.type * base.type * base.type
+ | prod_rect => base.type * base.type * base.type
| bool_rect => base.type
| nat_rect => base.type
| list_rect => base.type * base.type
@@ -1422,7 +1422,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| Compilers.ident.pair A B => tt
| Compilers.ident.fst A B => tt
| Compilers.ident.snd A B => tt
- | Compilers.ident.pair_rect A B T => tt
+ | Compilers.ident.prod_rect A B T => tt
| Compilers.ident.bool_rect T => tt
| Compilers.ident.nat_rect P => tt
| Compilers.ident.list_rect A P => tt
@@ -1503,7 +1503,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| pair, Compilers.ident.pair A B => Some (A, B)
| fst, Compilers.ident.fst A B => Some (A, B)
| snd, Compilers.ident.snd A B => Some (A, B)
- | pair_rect, Compilers.ident.pair_rect A B T => Some (A, B, T)
+ | prod_rect, Compilers.ident.prod_rect A B T => Some (A, B, T)
| bool_rect, Compilers.ident.bool_rect T => Some T
| nat_rect, Compilers.ident.nat_rect P => Some P
| list_rect, Compilers.ident.list_rect A P => Some (A, P)
@@ -1580,7 +1580,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| pair, _
| fst, _
| snd, _
- | pair_rect, _
+ | prod_rect, _
| bool_rect, _
| nat_rect, _
| list_rect, _
@@ -1665,7 +1665,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| pair => fun arg => let '(A, B) := eta2 arg in (type.base A -> type.base B -> type.base (A * B)%etype)
| fst => fun arg => let '(A, B) := eta2 arg in (type.base (A * B)%etype -> type.base A)
| snd => fun arg => let '(A, B) := eta2 arg in (type.base (A * B)%etype -> type.base B)
- | pair_rect => fun arg => let '(A, B, T) := eta3 arg in ((type.base A -> type.base B -> type.base T) -> type.base (A * B)%etype -> type.base T)
+ | prod_rect => fun arg => let '(A, B, T) := eta3 arg in ((type.base A -> type.base B -> type.base T) -> type.base (A * B)%etype -> type.base T)
| bool_rect => fun T => ((type.base ()%etype -> type.base T) -> (type.base ()%etype -> type.base T) -> type.base (base.type.type_base base.type.bool) -> type.base T)
| nat_rect => fun P => ((type.base ()%etype -> type.base P) -> (type.base (base.type.type_base base.type.nat) -> type.base P -> type.base P) -> type.base (base.type.type_base base.type.nat) -> type.base P)
| list_rect => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P -> type.base P) -> type.base (base.type.list A) -> type.base P)
@@ -1746,7 +1746,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| pair => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of pair args') with (A, B) => @Compilers.ident.pair A B end
| fst => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of fst args') with (A, B) => @Compilers.ident.fst A B end
| snd => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of snd args') with (A, B) => @Compilers.ident.snd A B end
- | pair_rect => fun arg => match eta3 arg as args' return Compilers.ident.ident (type_of pair_rect args') with (A, B, T) => @Compilers.ident.pair_rect A B T end
+ | prod_rect => fun arg => match eta3 arg as args' return Compilers.ident.ident (type_of prod_rect args') with (A, B, T) => @Compilers.ident.prod_rect A B T end
| bool_rect => fun T => @Compilers.ident.bool_rect T
| nat_rect => fun P => @Compilers.ident.nat_rect P
| list_rect => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of list_rect args') with (A, P) => @Compilers.ident.list_rect A P end
@@ -1827,7 +1827,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| Compilers.ident.pair A B => fun _ => @Compilers.ident.pair A B
| Compilers.ident.fst A B => fun _ => @Compilers.ident.fst A B
| Compilers.ident.snd A B => fun _ => @Compilers.ident.snd A B
- | Compilers.ident.pair_rect A B T => fun _ => @Compilers.ident.pair_rect A B T
+ | Compilers.ident.prod_rect A B T => fun _ => @Compilers.ident.prod_rect A B T
| Compilers.ident.bool_rect T => fun _ => @Compilers.ident.bool_rect T
| Compilers.ident.nat_rect P => fun _ => @Compilers.ident.nat_rect P
| Compilers.ident.list_rect A P => fun _ => @Compilers.ident.list_rect A P
diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v
index af9780418..f4defdb6f 100644
--- a/src/Experiments/NewPipeline/Language.v
+++ b/src/Experiments/NewPipeline/Language.v
@@ -5,6 +5,7 @@ Require Import Coq.Classes.Morphisms.
Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn.
Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil.
Require Import Crypto.Util.Option.
+Require Import Crypto.Util.Prod.
Require Import Crypto.Util.ZRange.
Require Import Crypto.Util.ZUtil.Definitions.
Require Import Crypto.Util.ZUtil.Notations.
@@ -517,13 +518,9 @@ Module Compilers.
| match ?b with true => ?t | false => ?f end
=> let T := type of term in
reify_rec (@bool_rect (fun _ => T) t f b)
- | match ?x with Datatypes.pair a b => ?f end
- => let x' := fresh in
- let T := type of x in
- reify_rec ((fun x' : T
- => match Datatypes.fst x, Datatypes.snd x return _ with
- | a, b => f
- end) x)
+ | match ?x with Datatypes.pair a b => @?f a b end
+ => let T := type of term in
+ reify_rec (@prod_rect _ _ (fun _ => T) f x)
| match ?x with nil => ?N | cons a b => @?C a b end
=> let T := type of term in
reify_rec (@list_case _ (fun _ => T) N C x)
@@ -761,7 +758,7 @@ Module Compilers.
| pair {A B:base.type} : ident (A -> B -> A * B)
| fst {A B} : ident (A * B -> A)
| snd {A B} : ident (A * B -> B)
- | pair_rect {A B T:base.type} : ident ((A -> B -> T) -> A * B -> T)
+ | prod_rect {A B T:base.type} : ident ((A -> B -> T) -> A * B -> T)
| bool_rect {T:base.type} : ident ((unit -> T) -> (unit -> T) -> bool -> T)
| nat_rect {P:base.type} : ident ((unit -> P) -> (nat -> P -> P) -> nat -> P)
| list_rect {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P -> P) -> list A -> P)
@@ -882,7 +879,7 @@ Module Compilers.
| pair A B => Datatypes.pair
| fst A B => Datatypes.fst
| snd A B => Datatypes.snd
- | pair_rect A B T => fun f '((a, b) : base.interp A * base.interp B) => f a b
+ | prod_rect A B T => fun f '((a, b) : base.interp A * base.interp B) => f a b
| bool_rect T
=> fun t f => Datatypes.bool_rect _ (t tt) (f tt)
| nat_rect P
@@ -968,8 +965,6 @@ Module Compilers.
(** TODO: MOVE ME? *)
Module Thunked.
- Definition pair_rect {A B} P (f : A -> B -> P) (x : A * B) : P
- := let '(a, b) := x in f a b.
Definition bool_rect P (t f : Datatypes.unit -> P) (b : bool) : P
:= Datatypes.bool_rect (fun _ => P) (t tt) (f tt) b.
Definition list_rect {A} P (N : Datatypes.unit -> P) (C : A -> list A -> P -> P) (ls : list A) : P
@@ -1050,6 +1045,11 @@ Module Compilers.
| @Thunked.bool_rect ?T
=> let rT := base.reify T in
then_tac (@ident.bool_rect rT)
+ | @Datatypes.prod_rect ?A ?B (fun _ => ?T)
+ => let rA := base.reify A in
+ let rB := base.reify B in
+ let rT := base.reify T in
+ then_tac (@ident.prod_rect rA rB rT)
| @Datatypes.nat_rect (fun _ => ?T) ?P0
=> reify_rec (@Thunked.nat_rect T (fun _ : Datatypes.unit => P0))
| @Thunked.nat_rect ?T
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index ec9e36c67..a3f9f4e8c 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -1167,7 +1167,7 @@ In the RHS, the follow notation applies:
then t ##tt
else f ##tt)
; make_rewrite
- (#pident.pair_rect @ ??{?? -> ?? -> ??} @ (??, ??))
+ (#pident.prod_rect @ ??{?? -> ?? -> ??} @ (??, ??))
(fun _ _ _ f _ x _ y
=> x <- castbe x; y <- castbe y; ret (f x y))
; make_rewrite
@@ -1192,7 +1192,7 @@ In the RHS, the follow notation applies:
([], [])
(fun x tl partition_tl
=> fx <-- f x;
- (#ident.pair_rect
+ (#ident.prod_rect
@ (λ g d, #ident.bool_rect
@ (λ _, ($x :: $g, $d))
@ (λ _, ($g, $x :: $d))
diff --git a/src/Experiments/NewPipeline/fancy_rewrite_head.out b/src/Experiments/NewPipeline/fancy_rewrite_head.out
index bf0910253..2201473ab 100644
--- a/src/Experiments/NewPipeline/fancy_rewrite_head.out
+++ b/src/Experiments/NewPipeline/fancy_rewrite_head.out
@@ -43,14 +43,14 @@ match idc in (ident t) return (Compile.value' true t) with
| @ident.snd A B =>
fun x : expr (type.base (A * B)%etype) =>
UnderLets.Base (#(ident.snd)%expr @ x)%expr_pat
-| @ident.pair_rect A B T =>
+| @ident.prod_rect A B T =>
fun
(x : expr (type.base A) ->
expr (type.base B) ->
UnderLets.UnderLets base.type ident var (expr (type.base T)))
(x0 : expr (type.base (A * B)%etype)) =>
UnderLets.Base
- (#(ident.pair_rect)%expr @
+ (#(ident.prod_rect)%expr @
(λ (x1 : var (type.base A))(x2 : var (type.base B)),
UnderLets.to_expr (x ($x1) ($x2)))%expr @ x0)%expr_pat
| @ident.bool_rect T =>
diff --git a/src/Experiments/NewPipeline/rewrite_head.out b/src/Experiments/NewPipeline/rewrite_head.out
index 81a45b663..600c4cb58 100644
--- a/src/Experiments/NewPipeline/rewrite_head.out
+++ b/src/Experiments/NewPipeline/rewrite_head.out
@@ -355,7 +355,7 @@ match idc in (ident t) return (Compile.value' true t) with
UnderLets.Base (#(ident.snd)%expr @ x)%expr_pat
| _ => UnderLets.Base (#(ident.snd)%expr @ x)%expr_pat
end
-| @ident.pair_rect A B T =>
+| @ident.prod_rect A B T =>
fun
(x : expr (type.base A) ->
expr (type.base B) ->
@@ -365,7 +365,7 @@ match idc in (ident t) return (Compile.value' true t) with
| @expr.App _ _ _ s _ #(_)%expr_pat _ | @expr.App _ _ _ s _ ($_)%expr _ |
@expr.App _ _ _ s _ (@expr.Abs _ _ _ _ _ _) _ =>
UnderLets.Base
- (#(ident.pair_rect)%expr @
+ (#(ident.prod_rect)%expr @
(λ (x2 : var (type.base A))(x3 : var (type.base B)),
UnderLets.to_expr (x ($x2) ($x3)))%expr @ x0)%expr_pat
| @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ #(idc)%expr_pat x2) x1 =>
@@ -442,7 +442,7 @@ match idc in (ident t) return (Compile.value' true t) with
unwrap))
| None =>
UnderLets.Base
- (#(ident.pair_rect)%expr @
+ (#(ident.prod_rect)%expr @
(λ (x5 : var (type.base A))
(x6 : var (type.base B)),
UnderLets.to_expr
@@ -450,7 +450,7 @@ match idc in (ident t) return (Compile.value' true t) with
end))%under_lets
| None =>
UnderLets.Base
- (#(ident.pair_rect)%expr @
+ (#(ident.prod_rect)%expr @
(λ (x5 : var (type.base A))(x6 :
var
(type.base
@@ -460,7 +460,7 @@ match idc in (ident t) return (Compile.value' true t) with
end)
| None =>
UnderLets.Base
- (#(ident.pair_rect)%expr @
+ (#(ident.prod_rect)%expr @
(λ (x4 : var (type.base A))(x5 : var
(type.base B)),
UnderLets.to_expr (x ($x4) ($x5)))%expr @ x0)%expr_pat
@@ -469,49 +469,49 @@ match idc in (ident t) return (Compile.value' true t) with
fun _ : Compile.value' false s1 -> Compile.value' true d1
=>
UnderLets.Base
- (#(ident.pair_rect)%expr @
+ (#(ident.prod_rect)%expr @
(λ (x3 : var (type.base A))(x4 : var (type.base B)),
UnderLets.to_expr (x ($x3) ($x4)))%expr @ x0)%expr_pat
end (Compile.reflect x1)
| (s1 -> d1)%ptype =>
fun _ : Compile.value' false s1 -> Compile.value' true d1 =>
UnderLets.Base
- (#(ident.pair_rect)%expr @
+ (#(ident.prod_rect)%expr @
(λ (x3 : var (type.base A))(x4 : var (type.base B)),
UnderLets.to_expr (x ($x3) ($x4)))%expr @ x0)%expr_pat
end (Compile.reflect x2)
| None =>
UnderLets.Base
- (#(ident.pair_rect)%expr @
+ (#(ident.prod_rect)%expr @
(λ (x3 : var (type.base A))(x4 : var (type.base B)),
UnderLets.to_expr (x ($x3) ($x4)))%expr @ x0)%expr_pat
end
| @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ ($_)%expr _) _ | @expr.App _
_ _ s _ (@expr.App _ _ _ s0 _ (@expr.Abs _ _ _ _ _ _) _) _ =>
UnderLets.Base
- (#(ident.pair_rect)%expr @
+ (#(ident.prod_rect)%expr @
(λ (x3 : var (type.base A))(x4 : var (type.base B)),
UnderLets.to_expr (x ($x3) ($x4)))%expr @ x0)%expr_pat
| @expr.App _ _ _ s _ (@expr.App _ _ _ s0 _ (_ @ _)%expr_pat _) _ |
@expr.App _ _ _ s _
(@expr.App _ _ _ s0 _ (@expr.LetIn _ _ _ _ _ _ _) _) _ =>
UnderLets.Base
- (#(ident.pair_rect)%expr @
+ (#(ident.prod_rect)%expr @
(λ (x4 : var (type.base A))(x5 : var (type.base B)),
UnderLets.to_expr (x ($x4) ($x5)))%expr @ x0)%expr_pat
| @expr.App _ _ _ s _ (@expr.LetIn _ _ _ _ _ _ _) _ =>
UnderLets.Base
- (#(ident.pair_rect)%expr @
+ (#(ident.prod_rect)%expr @
(λ (x3 : var (type.base A))(x4 : var (type.base B)),
UnderLets.to_expr (x ($x3) ($x4)))%expr @ x0)%expr_pat
| @expr.LetIn _ _ _ _ _ _ _ =>
UnderLets.Base
- (#(ident.pair_rect)%expr @
+ (#(ident.prod_rect)%expr @
(λ (x2 : var (type.base A))(x3 : var (type.base B)),
UnderLets.to_expr (x ($x2) ($x3)))%expr @ x0)%expr_pat
| _ =>
UnderLets.Base
- (#(ident.pair_rect)%expr @
+ (#(ident.prod_rect)%expr @
(λ (x1 : var (type.base A))(x2 : var (type.base B)),
UnderLets.to_expr (x ($x1) ($x2)))%expr @ x0)%expr_pat
end
@@ -1471,7 +1471,7 @@ match idc in (ident t) return (Compile.value' true t) with
rec' <-- rec;
fx <-- id x x1;
UnderLets.Base
- (#(ident.pair_rect)%expr @
+ (#(ident.prod_rect)%expr @
(λ g
d : expr
(type.base
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 14:31:33 +0000