aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/Experiments/NewPipeline/AbstractInterpretation.v4
-rw-r--r--src/Experiments/NewPipeline/CStringification.v8
-rw-r--r--src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v40
-rw-r--r--src/Experiments/NewPipeline/Language.v10
-rw-r--r--src/Experiments/NewPipeline/Rewriter.v10
5 files changed, 72 insertions, 0 deletions
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
@@ -1174,6 +1174,16 @@ In the RHS, the follow notation applies:
(??{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
=> xs <- reflect_list_cps xs;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 04:40:34 +0000