From 0fe3fa88a9c9434b03dfc642ddca8c6b05b9472c Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Wed, 18 Jul 2018 15:38:50 -0400
Subject: Support reification of firstn, skipn

---
 .../NewPipeline/AbstractInterpretation.v           |  4 +++
 src/Experiments/NewPipeline/CStringification.v     |  8 +++++
 .../NewPipeline/GENERATEDIdentifiersWithoutTypes.v | 40 ++++++++++++++++++++++
 src/Experiments/NewPipeline/Language.v             | 10 ++++++
 src/Experiments/NewPipeline/Rewriter.v             | 10 ++++++
 5 files changed, 72 insertions(+)

diff --git a/src/Experiments/NewPipeline/AbstractInterpretation.v b/src/Experiments/NewPipeline/AbstractInterpretation.v
index e550ae150..d018d63bb 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretation.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretation.v
@@ -373,6 +373,10 @@ Module Compilers.
                => fun x y => x <- x; y <- y; rSome (ident.interp idc x y)
              | ident.List_repeat _
                => fun x y => y <- y; Some (repeat x y)
+             | ident.List_firstn _
+               => fun n ls => n <- n; ls <- ls; Some (firstn n ls)
+             | ident.List_skipn _
+               => fun n ls => n <- n; ls <- ls; Some (skipn n ls)
              | ident.List_combine _ _
                => fun x y => x <- x; y <- y; Some (List.combine x y)
              | ident.List_flat_map _ _
diff --git a/src/Experiments/NewPipeline/CStringification.v b/src/Experiments/NewPipeline/CStringification.v
index ffe23f2ef..5f4f78243 100644
--- a/src/Experiments/NewPipeline/CStringification.v
+++ b/src/Experiments/NewPipeline/CStringification.v
@@ -232,6 +232,10 @@ Module Compilers.
                => fun args => (show_application with_casts (fun _ => "seq") args, ZRange.type.base.option.None)
              | ident.List_repeat A
                => fun args => (show_application with_casts (fun _ => "repeat") args, ZRange.type.base.option.None)
+             | ident.List_firstn A
+               => fun args => (show_application with_casts (fun _ => "firstn") args, ZRange.type.base.option.None)
+             | ident.List_skipn A
+               => fun args => (show_application with_casts (fun _ => "skipn") args, ZRange.type.base.option.None)
              | ident.List_combine A B
                => fun args => (show_application with_casts (fun _ => "combine") args, ZRange.type.base.option.None)
              | ident.List_map A B
@@ -350,6 +354,8 @@ Module Compilers.
                 | ident.List_length T => "length"
                 | ident.List_seq => "seq"
                 | ident.List_repeat A => "repeat"
+                | ident.List_firstn A => "firstn"
+                | ident.List_skipn A => "skipn"
                 | ident.List_combine A B => "combine"
                 | ident.List_map A B => "map"
                 | ident.List_app A => "(++)"
@@ -1144,6 +1150,8 @@ Module Compilers.
                | ident.List_length _
                | ident.List_seq
                | ident.List_repeat _
+               | ident.List_firstn _
+               | ident.List_skipn _
                | ident.List_combine _ _
                | ident.List_map _ _
                | ident.List_app _
diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
index a6ad5a725..5c6b4faec 100644
--- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
+++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
@@ -154,6 +154,18 @@ print_ident = r"""Inductive ident : defaults.type -> Set :=
                     (base.type.type_base base.type.nat) ->
                   (fun x : base.type => type.base x)
                     (base.type.list (base.type.type_base base.type.nat)))
+  | List_firstn : forall A : base.type,
+                  ident
+                    ((fun x : base.type => type.base x)
+                       (base.type.type_base base.type.nat) ->
+                     (fun x : base.type => type.base x) (base.type.list A) ->
+                     (fun x : base.type => type.base x) (base.type.list A))
+  | List_skipn : forall A : base.type,
+                 ident
+                   ((fun x : base.type => type.base x)
+                      (base.type.type_base base.type.nat) ->
+                    (fun x : base.type => type.base x) (base.type.list A) ->
+                    (fun x : base.type => type.base x) (base.type.list A))
   | List_repeat : forall A : base.type,
                   ident
                     ((fun x : base.type => type.base x) A ->
@@ -589,6 +601,8 @@ show_match_ident = r"""match # with
  | ident.list_case A P =>
  | ident.List_length T =>
  | ident.List_seq =>
+ | ident.List_firstn A =>
+ | ident.List_skipn A =>
  | ident.List_repeat A =>
  | ident.List_combine A B =>
  | ident.List_map A B =>
@@ -879,6 +893,8 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
       | list_case
       | List_length
       | List_seq
+      | List_firstn
+      | List_skipn
       | List_repeat
       | List_combine
       | List_map
@@ -960,6 +976,8 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | list_case, list_case
            | List_length, List_length
            | List_seq, List_seq
+           | List_firstn, List_firstn
+           | List_skipn, List_skipn
            | List_repeat, List_repeat
            | List_combine, List_combine
            | List_map, List_map
@@ -1039,6 +1057,8 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | list_case, _
            | List_length, _
            | List_seq, _
+           | List_firstn, _
+           | List_skipn, _
            | List_repeat, _
            | List_combine, _
            | List_map, _
@@ -1124,6 +1144,8 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | Compilers.ident.list_case A P => f _ (@Compilers.ident.list_case A P)
            | Compilers.ident.List_length T => f _ (@Compilers.ident.List_length T)
            | Compilers.ident.List_seq => f _ Compilers.ident.List_seq
+           | Compilers.ident.List_firstn A => f _ (@Compilers.ident.List_firstn A)
+           | Compilers.ident.List_skipn A => f _ (@Compilers.ident.List_skipn A)
            | Compilers.ident.List_repeat A => f _ (@Compilers.ident.List_repeat A)
            | Compilers.ident.List_combine A B => f _ (@Compilers.ident.List_combine A B)
            | Compilers.ident.List_map A B => f _ (@Compilers.ident.List_map A B)
@@ -1206,6 +1228,8 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | Compilers.ident.list_case A P => list_case
            | Compilers.ident.List_length T => List_length
            | Compilers.ident.List_seq => List_seq
+           | Compilers.ident.List_firstn A => List_firstn
+           | Compilers.ident.List_skipn A => List_skipn
            | Compilers.ident.List_repeat A => List_repeat
            | Compilers.ident.List_combine A B => List_combine
            | Compilers.ident.List_map A B => List_map
@@ -1288,6 +1312,8 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | list_case => None
            | List_length => None
            | List_seq => None
+           | List_firstn => None
+           | List_skipn => None
            | List_repeat => None
            | List_combine => None
            | List_map => None
@@ -1370,6 +1396,8 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | list_case => base.type * base.type
            | List_length => base.type
            | List_seq => unit
+           | List_firstn => base.type
+           | List_skipn => base.type
            | List_repeat => base.type
            | List_combine => base.type * base.type
            | List_map => base.type * base.type
@@ -1452,6 +1480,8 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | Compilers.ident.list_case A P => tt
            | Compilers.ident.List_length T => tt
            | Compilers.ident.List_seq => tt
+           | Compilers.ident.List_firstn A => tt
+           | Compilers.ident.List_skipn A => tt
            | Compilers.ident.List_repeat A => tt
            | Compilers.ident.List_combine A B => tt
            | Compilers.ident.List_map A B => tt
@@ -1534,6 +1564,8 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | list_case, Compilers.ident.list_case A P => Some (A, P)
            | List_length, Compilers.ident.List_length T => Some T
            | List_seq, Compilers.ident.List_seq => Some tt
+           | List_firstn, Compilers.ident.List_firstn A => Some A
+           | List_skipn, Compilers.ident.List_skipn A => Some A
            | List_repeat, Compilers.ident.List_repeat A => Some A
            | List_combine, Compilers.ident.List_combine A B => Some (A, B)
            | List_map, Compilers.ident.List_map A B => Some (A, B)
@@ -1612,6 +1644,8 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | list_case, _
            | List_length, _
            | List_seq, _
+           | List_firstn, _
+           | List_skipn, _
            | List_repeat, _
            | List_combine, _
            | List_map, _
@@ -1698,6 +1732,8 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | list_case => 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 (base.type.list A) -> type.base P)
            | List_length => fun T => (type.base (base.type.list T) -> type.base (base.type.type_base base.type.nat))
            | List_seq => fun _ => (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.list (base.type.type_base base.type.nat)))
+           | List_firstn => fun A => (type.base (base.type.type_base base.type.nat) -> type.base (base.type.list A) -> type.base (base.type.list A))
+           | List_skipn => fun A => (type.base (base.type.type_base base.type.nat) -> type.base (base.type.list A) -> type.base (base.type.list A))
            | List_repeat => fun A => (type.base A -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.list A))
            | List_combine => fun arg => let '(A, B) := eta2 arg in (type.base (base.type.list A) -> type.base (base.type.list B) -> type.base (base.type.list (A * B)))
            | List_map => fun arg => let '(A, B) := eta2 arg in ((type.base A -> type.base B) -> type.base (base.type.list A) -> type.base (base.type.list B))
@@ -1780,6 +1816,8 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | list_case => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of list_case args') with (A, P) => @Compilers.ident.list_case A P end
            | List_length => fun T => @Compilers.ident.List_length T
            | List_seq => fun _ => @Compilers.ident.List_seq
+           | List_firstn => fun A => @Compilers.ident.List_firstn A
+           | List_skipn => fun A => @Compilers.ident.List_skipn A
            | List_repeat => fun A => @Compilers.ident.List_repeat A
            | List_combine => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of List_combine args') with (A, B) => @Compilers.ident.List_combine A B end
            | List_map => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of List_map args') with (A, B) => @Compilers.ident.List_map A B end
@@ -1862,6 +1900,8 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | Compilers.ident.list_case A P => fun _ => @Compilers.ident.list_case A P
            | Compilers.ident.List_length T => fun _ => @Compilers.ident.List_length T
            | Compilers.ident.List_seq => fun _ => @Compilers.ident.List_seq
+           | Compilers.ident.List_firstn A => fun _ => @Compilers.ident.List_firstn A
+           | Compilers.ident.List_skipn A => fun _ => @Compilers.ident.List_skipn A
            | Compilers.ident.List_repeat A => fun _ => @Compilers.ident.List_repeat A
            | Compilers.ident.List_combine A B => fun _ => @Compilers.ident.List_combine A B
            | Compilers.ident.List_map A B => fun _ => @Compilers.ident.List_map A B
diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v
index 08da2ff6c..971ae81ef 100644
--- a/src/Experiments/NewPipeline/Language.v
+++ b/src/Experiments/NewPipeline/Language.v
@@ -766,6 +766,8 @@ Module Compilers.
         | list_case {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P) -> list A -> P)
         | List_length {T} : ident (list T -> nat)
         | List_seq : ident (nat -> nat -> list nat)
+        | List_firstn {A:base.type} : ident (nat -> list A -> list A)
+        | List_skipn {A:base.type} : ident (nat -> list A -> list A)
         | List_repeat {A:base.type} : ident (A -> nat -> list A)
         | List_combine {A B} : ident (list A -> list B -> list (A * B))
         | List_map {A B:base.type} : ident ((A -> B) -> list A -> list B)
@@ -893,6 +895,8 @@ Module Compilers.
                => fun N_case C_case => ListUtil.list_case _ (N_case tt) C_case
              | List_length T => @List.length _
              | List_seq => List.seq
+             | List_firstn A => @List.firstn _
+             | List_skipn A => @List.skipn _
              | List_repeat A => @repeat _
              | List_combine A B => @List.combine _ _
              | List_map A B => @List.map _ _
@@ -1081,6 +1085,12 @@ Module Compilers.
           let rA := base.reify A in
           then_tac (@ident.List_length rA)
         | List.seq => then_tac ident.List_seq
+        | @List.firstn ?A
+          => let rA := base.reify A in
+             then_tac (@ident.List_firstn rA)
+        | @List.skipn ?A
+          => let rA := base.reify A in
+             then_tac (@ident.List_skipn rA)
         | @repeat ?A
           => let rA := base.reify A in
              then_tac (@ident.List_repeat rA)
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index 5fe127ca0..599a7d34e 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -1173,6 +1173,16 @@ In the RHS, the follow notation applies:
                 ; make_rewrite
                     (??{list ??} ++ ??{list ??})
                     (fun _ xs _ ys => rlist_rect_cast ys (fun x _ xs_ys => x :: xs_ys) xs)
+                ; make_rewrite
+                    (#pident.List_firstn @ #?ℕ @ ??{list ??})
+                    (fun n _ xs
+                     => xs <- reflect_list_cps xs;
+                          reify_list (List.firstn n xs))
+                ; make_rewrite
+                    (#pident.List_skipn @ #?ℕ @ ??{list ??})
+                    (fun n _ xs
+                     => xs <- reflect_list_cps xs;
+                          reify_list (List.skipn n xs))
                 ; make_rewrite
                     (#pident.List_rev @ ??{list ??})
                     (fun _ xs
-- 
cgit v1.2.3