aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/AbstractInterpretation.v5
-rw-r--r--src/CStringification.v4
-rw-r--r--src/GENERATEDIdentifiersWithoutTypes.v32
-rw-r--r--src/Language.v36
4 files changed, 62 insertions, 15 deletions
diff --git a/src/AbstractInterpretation.v b/src/AbstractInterpretation.v
index 808128025..ca0cb68bd 100644
--- a/src/AbstractInterpretation.v
+++ b/src/AbstractInterpretation.v
@@ -520,8 +520,8 @@ Module Compilers.
n
| None => ZRange.type.base.option.None
end
- | ident.eager_nat_rect_arrow _ _
| ident.nat_rect_arrow _ _
+ | ident.eager_nat_rect_arrow _ _
=> fun O_case S_case n v
=> match n with
| Some n
@@ -533,8 +533,8 @@ Module Compilers.
v
| None => ZRange.type.base.option.None
end
- | ident.eager_list_rect _ _
| ident.list_rect _ _
+ | ident.eager_list_rect _ _
=> fun N C ls
=> match ls with
| Some ls
@@ -545,6 +545,7 @@ Module Compilers.
ls
| None => ZRange.type.base.option.None
end
+ | ident.list_rect_arrow _ _ _
| ident.eager_list_rect_arrow _ _ _
=> fun N C ls v
=> match ls with
diff --git a/src/CStringification.v b/src/CStringification.v
index 3560a5f82..ff455130b 100644
--- a/src/CStringification.v
+++ b/src/CStringification.v
@@ -253,6 +253,8 @@ Module Compilers.
=> fun args => (show_application with_casts (fun _ => "list_rect") args, ZRange.type.base.option.None)
| ident.eager_list_rect A P
=> fun args => (show_application with_casts (fun _ => "eager_list_rect") args, ZRange.type.base.option.None)
+ | ident.list_rect_arrow A P Q
+ => fun args => (show_application with_casts (fun _ => "list_rect(→)") args, ZRange.type.base.option.None)
| ident.eager_list_rect_arrow A P Q
=> fun args => (show_application with_casts (fun _ => "eager_list_rect(→)") args, ZRange.type.base.option.None)
| ident.list_case A P
@@ -394,6 +396,7 @@ Module Compilers.
| ident.eager_nat_rect_arrow P Q => "eager_nat_rect(→)"
| ident.list_rect A P => "list_rect"
| ident.eager_list_rect A P => "eager_list_rect"
+ | ident.list_rect_arrow A P Q => "list_rect(→)"
| ident.eager_list_rect_arrow A P Q => "eager_list_rect(→)"
| ident.list_case A P => "list_case"
| ident.List_length T => "length"
@@ -1300,6 +1303,7 @@ Module Compilers.
| ident.option_rect _ _
| ident.list_rect _ _
| ident.eager_list_rect _ _
+ | ident.list_rect_arrow _ _ _
| ident.eager_list_rect_arrow _ _ _
| ident.list_case _ _
| ident.List_length _
diff --git a/src/GENERATEDIdentifiersWithoutTypes.v b/src/GENERATEDIdentifiersWithoutTypes.v
index c250253e1..db84a33a3 100644
--- a/src/GENERATEDIdentifiersWithoutTypes.v
+++ b/src/GENERATEDIdentifiersWithoutTypes.v
@@ -276,6 +276,21 @@ print_ident = r"""Inductive ident : defaults.type -> Set :=
(fun x : Compilers.base.type => type.base x)
(Compilers.base.type.list A) ->
(fun x : Compilers.base.type => type.base x) P)%ptype
+ | list_rect_arrow : forall A P Q : Compilers.base.type,
+ ident
+ (((fun x : Compilers.base.type => type.base x) P ->
+ (fun x : Compilers.base.type => type.base x) Q) ->
+ ((fun x : Compilers.base.type => type.base x) A ->
+ (fun x : Compilers.base.type => type.base x)
+ (Compilers.base.type.list A) ->
+ ((fun x : Compilers.base.type => type.base x) P ->
+ (fun x : Compilers.base.type => type.base x) Q) ->
+ (fun x : Compilers.base.type => type.base x) P ->
+ (fun x : Compilers.base.type => type.base x) Q) ->
+ (fun x : Compilers.base.type => type.base x)
+ (Compilers.base.type.list A) ->
+ (fun x : Compilers.base.type => type.base x) P ->
+ (fun x : Compilers.base.type => type.base x) Q)%ptype
| eager_list_rect : forall A P : Compilers.base.type,
ident
(((fun x : Compilers.base.type => type.base x)
@@ -865,6 +880,7 @@ show_match_ident = r"""match # with
| ident.eager_nat_rect P =>
| ident.eager_nat_rect_arrow P Q =>
| ident.list_rect A P =>
+ | ident.list_rect_arrow A P Q =>
| ident.eager_list_rect A P =>
| ident.eager_list_rect_arrow A P Q =>
| ident.list_case A P =>
@@ -1475,6 +1491,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| eager_nat_rect
| eager_nat_rect_arrow
| list_rect
+ | list_rect_arrow
| eager_list_rect
| eager_list_rect_arrow
| list_case
@@ -1569,6 +1586,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| eager_nat_rect => Compilers.base.type
| eager_nat_rect_arrow => Compilers.base.type * Compilers.base.type
| list_rect => Compilers.base.type * Compilers.base.type
+ | list_rect_arrow => Compilers.base.type * Compilers.base.type * Compilers.base.type
| eager_list_rect => Compilers.base.type * Compilers.base.type
| eager_list_rect_arrow => Compilers.base.type * Compilers.base.type * Compilers.base.type
| list_case => Compilers.base.type * Compilers.base.type
@@ -1664,6 +1682,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| eager_nat_rect => false
| eager_nat_rect_arrow => false
| list_rect => false
+ | list_rect_arrow => false
| eager_list_rect => false
| eager_list_rect_arrow => false
| list_case => false
@@ -1759,6 +1778,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| eager_nat_rect, Compilers.ident.eager_nat_rect P => Datatypes.Some P
| eager_nat_rect_arrow, Compilers.ident.eager_nat_rect_arrow P Q => Datatypes.Some (P, Q)
| list_rect, Compilers.ident.list_rect A P => Datatypes.Some (A, P)
+ | list_rect_arrow, Compilers.ident.list_rect_arrow A P Q => Datatypes.Some (A, P, Q)
| eager_list_rect, Compilers.ident.eager_list_rect A P => Datatypes.Some (A, P)
| eager_list_rect_arrow, Compilers.ident.eager_list_rect_arrow A P Q => Datatypes.Some (A, P, Q)
| list_case, Compilers.ident.list_case A P => Datatypes.Some (A, P)
@@ -1850,6 +1870,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| eager_nat_rect, _
| eager_nat_rect_arrow, _
| list_rect, _
+ | list_rect_arrow, _
| eager_list_rect, _
| eager_list_rect_arrow, _
| list_case, _
@@ -1946,6 +1967,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| eager_nat_rect => fun P => ((type.base ()%etype -> type.base P) -> (type.base (Compilers.base.type.type_base base.type.nat) -> type.base P -> type.base P) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base P)%ptype
| eager_nat_rect_arrow => fun arg => let '(P, Q) := eta2 arg in ((type.base P -> type.base Q) -> (type.base (Compilers.base.type.type_base base.type.nat) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base P -> type.base Q)%ptype
| list_rect => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype
+ | list_rect_arrow => fun arg => let '(A, P, Q) := eta3 arg in ((type.base P -> type.base Q) -> (type.base A -> type.base (Compilers.base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.list A) -> type.base P -> type.base Q)%ptype
| eager_list_rect => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype
| eager_list_rect_arrow => fun arg => let '(A, P, Q) := eta3 arg in ((type.base P -> type.base Q) -> (type.base A -> type.base (Compilers.base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.list A) -> type.base P -> type.base Q)%ptype
| list_case => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype
@@ -2041,6 +2063,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| eager_nat_rect => fun P => @Compilers.ident.eager_nat_rect P
| eager_nat_rect_arrow => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of eager_nat_rect_arrow arg') with (P, Q) => @Compilers.ident.eager_nat_rect_arrow P Q end
| list_rect => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of list_rect arg') with (A, P) => @Compilers.ident.list_rect A P end
+ | list_rect_arrow => fun arg => match eta3 arg as arg' return Compilers.ident.ident (type_of list_rect_arrow arg') with (A, P, Q) => @Compilers.ident.list_rect_arrow A P Q end
| eager_list_rect => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of eager_list_rect arg') with (A, P) => @Compilers.ident.eager_list_rect A P end
| eager_list_rect_arrow => fun arg => match eta3 arg as arg' return Compilers.ident.ident (type_of eager_list_rect_arrow arg') with (A, P, Q) => @Compilers.ident.eager_list_rect_arrow A P Q end
| list_case => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of list_case arg') with (A, P) => @Compilers.ident.list_case A P end
@@ -2143,6 +2166,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| Compilers.ident.eager_nat_rect P => f _ (@Compilers.ident.eager_nat_rect P)
| Compilers.ident.eager_nat_rect_arrow P Q => f _ (@Compilers.ident.eager_nat_rect_arrow P Q)
| Compilers.ident.list_rect A P => f _ (@Compilers.ident.list_rect A P)
+ | Compilers.ident.list_rect_arrow A P Q => f _ (@Compilers.ident.list_rect_arrow A P Q)
| Compilers.ident.eager_list_rect A P => f _ (@Compilers.ident.eager_list_rect A P)
| Compilers.ident.eager_list_rect_arrow A P Q => f _ (@Compilers.ident.eager_list_rect_arrow A P Q)
| Compilers.ident.list_case A P => f _ (@Compilers.ident.list_case A P)
@@ -2237,6 +2261,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| eager_nat_rect {P : base.type} : ident ((type.base ()%pbtype -> 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)%ptype
| eager_nat_rect_arrow {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base (base.type.type_base base.type.nat) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.type_base base.type.nat) -> type.base P -> type.base Q)%ptype
| list_rect {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> 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)%ptype
+ | list_rect_arrow {A : base.type} {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base A -> type.base (base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.list A) -> type.base P -> type.base Q)%ptype
| eager_list_rect {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> 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)%ptype
| eager_list_rect_arrow {A : base.type} {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base A -> type.base (base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.list A) -> type.base P -> type.base Q)%ptype
| list_case {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P) -> type.base (base.type.list A) -> type.base P)%ptype
@@ -2331,6 +2356,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| @eager_nat_rect P => Raw.ident.eager_nat_rect
| @eager_nat_rect_arrow P Q => Raw.ident.eager_nat_rect_arrow
| @list_rect A P => Raw.ident.list_rect
+ | @list_rect_arrow A P Q => Raw.ident.list_rect_arrow
| @eager_list_rect A P => Raw.ident.eager_list_rect
| @eager_list_rect_arrow A P Q => Raw.ident.eager_list_rect_arrow
| @list_case A P => Raw.ident.list_case
@@ -2426,6 +2452,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| @eager_nat_rect P => []
| @eager_nat_rect_arrow P Q => []
| @list_rect A P => []
+ | @list_rect_arrow A P Q => []
| @eager_list_rect A P => []
| @eager_list_rect_arrow A P Q => []
| @list_case A P => []
@@ -2521,6 +2548,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| @eager_nat_rect P => fun _ => @Compilers.ident.eager_nat_rect _
| @eager_nat_rect_arrow P Q => fun _ => @Compilers.ident.eager_nat_rect_arrow _ _
| @list_rect A P => fun _ => @Compilers.ident.list_rect _ _
+ | @list_rect_arrow A P Q => fun _ => @Compilers.ident.list_rect_arrow _ _ _
| @eager_list_rect A P => fun _ => @Compilers.ident.eager_list_rect _ _
| @eager_list_rect_arrow A P Q => fun _ => @Compilers.ident.eager_list_rect_arrow _ _ _
| @list_case A P => fun _ => @Compilers.ident.list_case _ _
@@ -2620,6 +2648,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| @eager_nat_rect P, Compilers.ident.eager_nat_rect P' => Datatypes.Some tt
| @eager_nat_rect_arrow P Q, Compilers.ident.eager_nat_rect_arrow P' Q' => Datatypes.Some tt
| @list_rect A P, Compilers.ident.list_rect A' P' => Datatypes.Some tt
+ | @list_rect_arrow A P Q, Compilers.ident.list_rect_arrow A' P' Q' => Datatypes.Some tt
| @eager_list_rect A P, Compilers.ident.eager_list_rect A' P' => Datatypes.Some tt
| @eager_list_rect_arrow A P Q, Compilers.ident.eager_list_rect_arrow A' P' Q' => Datatypes.Some tt
| @list_case A P, Compilers.ident.list_case A' P' => Datatypes.Some tt
@@ -2711,6 +2740,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| @eager_nat_rect _, _
| @eager_nat_rect_arrow _ _, _
| @list_rect _ _, _
+ | @list_rect_arrow _ _ _, _
| @eager_list_rect _ _, _
| @eager_list_rect_arrow _ _ _, _
| @list_case _ _, _
@@ -2807,6 +2837,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| Compilers.ident.eager_nat_rect P => @eager_nat_rect (base.relax P)
| Compilers.ident.eager_nat_rect_arrow P Q => @eager_nat_rect_arrow (base.relax P) (base.relax Q)
| Compilers.ident.list_rect A P => @list_rect (base.relax A) (base.relax P)
+ | Compilers.ident.list_rect_arrow A P Q => @list_rect_arrow (base.relax A) (base.relax P) (base.relax Q)
| Compilers.ident.eager_list_rect A P => @eager_list_rect (base.relax A) (base.relax P)
| Compilers.ident.eager_list_rect_arrow A P Q => @eager_list_rect_arrow (base.relax A) (base.relax P) (base.relax Q)
| Compilers.ident.list_case A P => @list_case (base.relax A) (base.relax P)
@@ -2902,6 +2933,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| Compilers.ident.eager_nat_rect P => tt
| Compilers.ident.eager_nat_rect_arrow P Q => tt
| Compilers.ident.list_rect A P => tt
+ | Compilers.ident.list_rect_arrow A P Q => tt
| Compilers.ident.eager_list_rect A P => tt
| Compilers.ident.eager_list_rect_arrow A P Q => tt
| Compilers.ident.list_case A P => tt
diff --git a/src/Language.v b/src/Language.v
index 695073248..74c34b2f2 100644
--- a/src/Language.v
+++ b/src/Language.v
@@ -880,6 +880,7 @@ Module Compilers.
| eager_nat_rect {P:base.type} : ident ((unit -> P) -> (nat -> P -> P) -> nat -> P)
| eager_nat_rect_arrow {P Q:base.type} : ident ((P -> Q) -> (nat -> (P -> Q) -> (P -> Q)) -> nat -> P -> Q)
| list_rect {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P -> P) -> list A -> P)
+ | list_rect_arrow {A P Q:base.type} : ident ((P -> Q) -> (A -> list A -> (P -> Q) -> (P -> Q)) -> list A -> P -> Q)
| eager_list_rect {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P -> P) -> list A -> P)
| eager_list_rect_arrow {A P Q:base.type} : ident ((P -> Q) -> (A -> list A -> (P -> Q) -> (P -> Q)) -> list A -> P -> Q)
| list_case {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P) -> list A -> P)
@@ -1058,17 +1059,15 @@ Module Compilers.
| bool_rect T
=> fun t f => Datatypes.bool_rect _ (t tt) (f tt)
| nat_rect P
- => fun O_case S_case => Datatypes.nat_rect _ (O_case tt) S_case
- | nat_rect_arrow P Q
- => fun O_case S_case => Datatypes.nat_rect _ O_case S_case
| eager_nat_rect P
=> fun O_case S_case => Datatypes.nat_rect _ (O_case tt) S_case
+ | nat_rect_arrow P Q
| eager_nat_rect_arrow P Q
=> fun O_case S_case => Datatypes.nat_rect _ O_case S_case
| list_rect A P
- => fun N_case C_case => Datatypes.list_rect _ (N_case tt) C_case
| eager_list_rect A P
=> fun N_case C_case => Datatypes.list_rect _ (N_case tt) C_case
+ | list_rect_arrow A P Q
| eager_list_rect_arrow A P Q
=> fun N_case C_case => Datatypes.list_rect _ N_case C_case
| list_case A P
@@ -1294,13 +1293,13 @@ Module Compilers.
end
| @Datatypes.nat_rect ?T0
=> lazymatch (eval cbv beta in T0) with
- | (fun _ => ?P -> ?Q)
- => let rP := base.reify P in
- let rQ := base.reify Q in
- then_tac (@ident.nat_rect_arrow rP rQ)
+ | (fun _ => ?P -> ?Q)
+ => let rP := base.reify P in
+ let rQ := base.reify Q in
+ then_tac (@ident.nat_rect_arrow rP rQ)
| T0 => else_tac ()
| ?T' => reify_rec (@Datatypes.nat_rect T')
- end
+ end
| @Thunked.nat_rect ?T
=> let rT := base.reify T in
then_tac (@ident.nat_rect rT)
@@ -1325,10 +1324,21 @@ Module Compilers.
then_tac (@ident.eager_nat_rect rT)
| @Datatypes.list_rect ?A ?T0 ?Pnil
=> lazymatch (eval cbv beta in T0) with
- | fun _ => ?T => reify_rec (@Thunked.list_rect A T (fun _ : Datatypes.unit => Pnil))
- | T0 => else_tac ()
- | ?T' => reify_rec (@Datatypes.list_rect A T' Pnil)
- end
+ | fun _ => _ -> _ => else_tac ()
+ | fun _ => ?T => reify_rec (@Thunked.list_rect A T (fun _ : Datatypes.unit => Pnil))
+ | T0 => else_tac ()
+ | ?T' => reify_rec (@Datatypes.list_rect A T' Pnil)
+ end
+ | @Datatypes.list_rect ?A ?T0
+ => lazymatch (eval cbv beta in T0) with
+ | (fun _ => ?P -> ?Q)
+ => let rA := base.reify A in
+ let rP := base.reify P in
+ let rQ := base.reify Q in
+ then_tac (@ident.list_rect_arrow rA rP rQ)
+ | T0 => else_tac ()
+ | ?T' => reify_rec (@Datatypes.list_rect A T')
+ end
| @Thunked.list_rect ?A ?T
=> let rA := base.reify A in
let rT := base.reify T in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 01:03:52 +0000