aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-04-23 01:38:50 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2019-04-24 09:39:45 -0400
commit8a4d828e05bca153f12370d08d3b4ad404fbbee2 (patch)
treecd0b847c4d39cdd440d1c2a6833ae54ab5149067
parentecdfd03c636ab63e167fbe4fc4d7ab0ed5d9db74 (diff)
Do less reduction in GENERATEDIdentifiersWithoutTypes
Since more of the definitions are now done in Gallina, hopefully these should be easier to factor out / parameterize over the type of identifiers, now. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------- 21m28.78s | Total | 21m49.80s || -0m21.01s | -1.60% ----------------------------------------------------------------------------------------------- 0m22.98s | GENERATEDIdentifiersWithoutTypesProofs.vo | 0m49.53s || -0m26.55s | -53.60% 0m47.26s | p521_32.c | 0m44.08s || +0m03.17s | +7.21% 0m36.30s | ExtractionHaskell/saturated_solinas | 0m32.96s || +0m03.33s | +10.13% 1m00.34s | ExtractionHaskell/word_by_word_montgomery | 1m02.45s || -0m02.10s | -3.37% 0m26.90s | SlowPrimeSynthesisExamples.vo | 0m24.35s || +0m02.54s | +10.47% 0m16.06s | GENERATEDIdentifiersWithoutTypes.vo | 0m19.05s || -0m02.99s | -15.69% 0m14.89s | ExtractionOCaml/unsaturated_solinas | 0m12.83s || +0m02.06s | +16.05% 0m43.92s | ExtractionHaskell/unsaturated_solinas | 0m42.40s || +0m01.52s | +3.58% 0m20.11s | ExtractionOCaml/word_by_word_montgomery | 0m21.19s || -0m01.08s | -5.09% 0m20.06s | p256_32.c | 0m21.81s || -0m01.75s | -8.02% 0m17.96s | secp256k1_32.c | 0m19.45s || -0m01.48s | -7.66% 0m13.58s | ExtractionOCaml/word_by_word_montgomery.ml | 0m14.89s || -0m01.31s | -8.79% 0m07.27s | ExtractionOCaml/saturated_solinas.ml | 0m05.75s || +0m01.51s | +26.43% 3m23.62s | p384_32.c | 3m23.29s || +0m00.33s | +0.16% 1m42.18s | Fancy/Barrett256.vo | 1m41.69s || +0m00.49s | +0.48% 1m33.94s | RewriterWf2.vo | 1m34.43s || -0m00.49s | -0.51% 0m55.14s | Rewriter/ToFancyWithCasts.vo | 0m55.92s || -0m00.78s | -1.39% 0m46.15s | Rewriter/NBE.vo | 0m46.06s || +0m00.08s | +0.19% 0m44.70s | Rewriter/ArithWithCasts.vo | 0m44.55s || +0m00.15s | +0.33% 0m43.96s | RewriterInterpProofs1.vo | 0m44.18s || -0m00.21s | -0.49% 0m39.78s | p521_64.c | 0m38.84s || +0m00.93s | +2.42% 0m36.72s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.54s || +0m00.17s | +0.49% 0m35.92s | RewriterWf1.vo | 0m36.26s || -0m00.33s | -0.93% 0m34.57s | Fancy/Montgomery256.vo | 0m34.64s || -0m00.07s | -0.20% 0m27.29s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m27.17s || +0m00.11s | +0.44% 0m23.67s | Rewriter/Arith.vo | 0m24.59s || -0m00.91s | -3.74% 0m20.78s | PushButtonSynthesis/BarrettReduction.vo | 0m20.69s || +0m00.08s | +0.43% 0m18.97s | p448_solinas_64.c | 0m18.10s || +0m00.86s | +4.80% 0m14.02s | p434_64.c | 0m13.37s || +0m00.65s | +4.86% 0m11.26s | ExtractionOCaml/unsaturated_solinas.ml | 0m10.61s || +0m00.65s | +6.12% 0m10.76s | ExtractionOCaml/saturated_solinas | 0m11.65s || -0m00.89s | -7.63% 0m08.76s | p224_32.c | 0m09.58s || -0m00.82s | -8.55% 0m08.07s | ExtractionHaskell/word_by_word_montgomery.hs | 0m07.96s || +0m00.11s | +1.38% 0m07.88s | p384_64.c | 0m08.81s || -0m00.93s | -10.55% 0m06.98s | BoundsPipeline.vo | 0m06.97s || +0m00.01s | +0.14% 0m06.41s | ExtractionHaskell/unsaturated_solinas.hs | 0m05.52s || +0m00.89s | +16.12% 0m05.21s | ExtractionHaskell/saturated_solinas.hs | 0m04.48s || +0m00.72s | +16.29% 0m03.54s | PushButtonSynthesis/Primitives.vo | 0m03.61s || -0m00.06s | -1.93% 0m03.33s | PushButtonSynthesis/SmallExamples.vo | 0m03.38s || -0m00.04s | -1.47% 0m03.20s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.22s || -0m00.02s | -0.62% 0m03.05s | curve25519_32.c | 0m02.76s || +0m00.29s | +10.50% 0m02.63s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.70s || -0m00.07s | -2.59% 0m02.53s | Rewriter.vo | 0m02.04s || +0m00.48s | +24.01% 0m02.10s | curve25519_64.c | 0m01.80s || +0m00.30s | +16.66% 0m01.94s | p224_64.c | 0m01.52s || +0m00.41s | +27.63% 0m01.85s | secp256k1_64.c | 0m01.55s || +0m00.30s | +19.35% 0m01.40s | CLI.vo | 0m01.33s || +0m00.06s | +5.26% 0m01.36s | p256_64.c | 0m01.84s || -0m00.48s | -26.08% 0m01.33s | Rewriter/StripLiteralCasts.vo | 0m01.22s || +0m00.11s | +9.01% 0m01.23s | CompilersTestCases.vo | 0m01.14s || +0m00.09s | +7.89% 0m01.15s | StandaloneOCamlMain.vo | 0m01.11s || +0m00.03s | +3.60% 0m01.13s | StandaloneHaskellMain.vo | 0m01.17s || -0m00.04s | -3.41% 0m01.11s | Rewriter/ToFancy.vo | 0m01.07s || +0m00.04s | +3.73% 0m00.80s | RewriterAll.vo | 0m00.80s || +0m00.00s | +0.00% 0m00.74s | RewriterAllTactics.vo | 0m00.91s || -0m00.17s | -18.68% The diff in the .ml files is quite small, and is effectively just variable renaming: ```diff diff --git a/src/ExtractionOCaml/saturated_solinas.ml b/src/ExtractionOCaml/saturated_solinas.ml index fd8a9d3..e9afa49 100644 --- a/src/ExtractionOCaml/saturated_solinas.ml +++ b/src/ExtractionOCaml/saturated_solinas.ml @@ -39856,7 +39856,7 @@ module Coq2_Compilers = | Compilers.Coq_ident.Literal (t1, v) -> (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) @@ -39962,7 +39962,7 @@ module Coq2_Compilers = (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) @@ -40068,7 +40068,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v @@ -40174,7 +40174,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v | Compilers.Coq_ident.Nat_succ -> None @@ -40280,7 +40280,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> - (fun v0 -> Some (Obj.magic (v0, ())))) v + (fun x -> Some (Obj.magic (x, ())))) v | Compilers.Coq_ident.Nat_succ -> None | Compilers.Coq_ident.Nat_pred -> None | Compilers.Coq_ident.Nat_max -> None @@ -49466,8 +49466,8 @@ module Coq2_Compilers = | Compilers.Coq_ident.Coq_fancy_mullh _ -> None | Compilers.Coq_ident.Coq_fancy_mulhl _ -> None | Compilers.Coq_ident.Coq_fancy_mulhh _ -> None - | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, z0) -> - Some (Obj.magic (log2wordmax, (z0, ()))) + | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, x) -> + Some (Obj.magic (log2wordmax, (x, ()))) | Compilers.Coq_ident.Coq_fancy_selc -> None | Compilers.Coq_ident.Coq_fancy_selm _ -> None | Compilers.Coq_ident.Coq_fancy_sell -> None diff --git a/src/ExtractionOCaml/unsaturated_solinas.ml b/src/ExtractionOCaml/unsaturated_solinas.ml index 473992c..4d4d604 100644 --- a/src/ExtractionOCaml/unsaturated_solinas.ml +++ b/src/ExtractionOCaml/unsaturated_solinas.ml @@ -40045,7 +40045,7 @@ module Coq2_Compilers = | Compilers.Coq_ident.Literal (t1, v) -> (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) @@ -40151,7 +40151,7 @@ module Coq2_Compilers = (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) @@ -40257,7 +40257,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v @@ -40363,7 +40363,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v | Compilers.Coq_ident.Nat_succ -> None @@ -40469,7 +40469,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> - (fun v0 -> Some (Obj.magic (v0, ())))) v + (fun x -> Some (Obj.magic (x, ())))) v | Compilers.Coq_ident.Nat_succ -> None | Compilers.Coq_ident.Nat_pred -> None | Compilers.Coq_ident.Nat_max -> None @@ -49655,8 +49655,8 @@ module Coq2_Compilers = | Compilers.Coq_ident.Coq_fancy_mullh _ -> None | Compilers.Coq_ident.Coq_fancy_mulhl _ -> None | Compilers.Coq_ident.Coq_fancy_mulhh _ -> None - | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, z0) -> - Some (Obj.magic (log2wordmax, (z0, ()))) + | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, x) -> + Some (Obj.magic (log2wordmax, (x, ()))) | Compilers.Coq_ident.Coq_fancy_selc -> None | Compilers.Coq_ident.Coq_fancy_selm _ -> None | Compilers.Coq_ident.Coq_fancy_sell -> None diff --git a/src/ExtractionOCaml/word_by_word_montgomery.ml b/src/ExtractionOCaml/word_by_word_montgomery.ml index f955bc6..a672b5d 100644 --- a/src/ExtractionOCaml/word_by_word_montgomery.ml +++ b/src/ExtractionOCaml/word_by_word_montgomery.ml @@ -39944,7 +39944,7 @@ module Coq2_Compilers = | Compilers.Coq_ident.Literal (t1, v) -> (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) @@ -40050,7 +40050,7 @@ module Coq2_Compilers = (match t1 with | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) @@ -40156,7 +40156,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_unit -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v @@ -40262,7 +40262,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Z -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> - (fun v0 -> Some (Obj.magic (v0, ()))) + (fun x -> Some (Obj.magic (x, ()))) | Compilers.Coq_base.Coq_type.Coq_zrange -> (fun _ -> None)) v | Compilers.Coq_ident.Nat_succ -> None @@ -40368,7 +40368,7 @@ module Coq2_Compilers = | Compilers.Coq_base.Coq_type.Coq_bool -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_nat -> (fun _ -> None) | Compilers.Coq_base.Coq_type.Coq_zrange -> - (fun v0 -> Some (Obj.magic (v0, ())))) v + (fun x -> Some (Obj.magic (x, ())))) v | Compilers.Coq_ident.Nat_succ -> None | Compilers.Coq_ident.Nat_pred -> None | Compilers.Coq_ident.Nat_max -> None @@ -49554,8 +49554,8 @@ module Coq2_Compilers = | Compilers.Coq_ident.Coq_fancy_mullh _ -> None | Compilers.Coq_ident.Coq_fancy_mulhl _ -> None | Compilers.Coq_ident.Coq_fancy_mulhh _ -> None - | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, z0) -> - Some (Obj.magic (log2wordmax, (z0, ()))) + | Compilers.Coq_ident.Coq_fancy_rshi (log2wordmax, x) -> + Some (Obj.magic (log2wordmax, (x, ()))) | Compilers.Coq_ident.Coq_fancy_selc -> None | Compilers.Coq_ident.Coq_fancy_selm _ -> None | Compilers.Coq_ident.Coq_fancy_sell -> None ```
Diffstat
-rw-r--r--src/GENERATEDIdentifiersWithoutTypes.v677
-rw-r--r--src/GENERATEDIdentifiersWithoutTypesProofs.v472
-rw-r--r--src/Rewriter.v4
-rw-r--r--src/RewriterWf1.v11
4 files changed, 842 insertions, 322 deletions
diff --git a/src/GENERATEDIdentifiersWithoutTypes.v b/src/GENERATEDIdentifiersWithoutTypes.v
index a7763c0c1..111b88bef 100644
--- a/src/GENERATEDIdentifiersWithoutTypes.v
+++ b/src/GENERATEDIdentifiersWithoutTypes.v
@@ -1,5 +1,4 @@
Require Import Coq.ZArith.ZArith.
-Require Import Coq.Logic.JMeq.
Require Import Coq.FSets.FMapPositive.
Require Import Coq.MSets.MSetPositive.
Require Import Coq.Lists.List.
@@ -18,6 +17,7 @@ Require Crypto.Util.Tuple.
Import ListNotations. Local Open Scope list_scope.
Import PrimitiveSigma.Primitive.
+Import EqNotations.
Module Compilers.
Set Boolean Equality Schemes.
Set Decidable Equality Schemes.
@@ -66,8 +66,8 @@ Module Compilers.
| nil => fun x => x
| T :: Ts
=> fun v_vs
- => (F T (Datatypes.fst v_vs),
- @lift_type_of_list_map A Ts P1 P2 F (Datatypes.snd v_vs))
+ => (F T (fst v_vs),
+ @lift_type_of_list_map A Ts P1 P2 F (snd v_vs))
end.
Module pattern.
@@ -227,10 +227,28 @@ Module Compilers.
| _ => constr_fail_with ltac:(fun _ => fail 1 "Could not find" ctor "from" from_all_idents "(index" n ") in" to_all_idents "(failed to eliminate dependency on dummy default argument in" v ")")
end in
v.
+
+ Ltac make_ident_index ty all_idents :=
+ let all_idents := (eval hnf in all_idents) in
+ let v := (eval cbv [id] in
+ (ltac:(intros;
+ let idc := lazymatch goal with idc : _ |- _ => idc end in
+ let idc' := fresh "idc'" in
+ pose idc as idc';
+ destruct idc;
+ let idc := (eval cbv [idc'] in idc') in
+ let idc := head idc in
+ let n := get_ctor_number' idc all_idents in
+ exact n)
+ : ty)) in
+ refine v.
End Tactics.
Definition all_idents : list { T : Type & T } := ltac:(make_all_idents).
+ Definition ident_index : forall t, ident t -> nat
+ := ltac:(make_ident_index (forall t, ident t -> nat) all_idents).
+
Definition eta_ident_cps_gen
{T : forall t, Compilers.ident.ident t -> Type}
(f : forall t idc, T t idc)
@@ -246,24 +264,33 @@ Module Compilers.
Definition eta_ident_cps_gen2
{T0 : forall t, Compilers.ident.ident t -> Type}
(f0 : forall t idc, T0 t idc)
- {T1 : forall t (idc : Compilers.ident.ident t), T0 t idc -> Type}
+ {T1 : forall t idc, T0 t idc -> Type}
(f1 : forall t idc, T1 t idc (f0 t idc))
- : forall t idc, T1 t idc (proj1_sig (@eta_ident_cps_gen T0 f0) t idc).
- Proof. intros t idc; cbv [proj1_sig eta_ident_cps_gen]; destruct idc; exact (f1 _ _). Defined.
+ : { f' : forall t idc, T1 t idc (proj1_sig (@eta_ident_cps_gen T0 f0) t idc)
+ | forall t idc,
+ f' t idc = rew [T1 t idc] (eq_sym (proj2_sig (@eta_ident_cps_gen T0 f0) t idc)) in f1 t idc }.
+ Proof. apply eta_ident_cps_gen. Defined.
Definition eta_ident_cps_gen3
{T0 : forall t, Compilers.ident.ident t -> Type}
(f0 : forall t idc, T0 t idc)
- {T1 : forall t (idc : Compilers.ident.ident t), T0 t idc -> Type}
+ {T1 : forall t idc, T0 t idc -> Type}
(f1 : forall t idc, T1 t idc (f0 t idc))
{T2 : forall t idc x, T1 t idc x -> Type}
(f2 : forall t idc, T2 t idc (f0 t idc) (f1 t idc))
- : forall t idc, T2 t idc (proj1_sig (@eta_ident_cps_gen T0 f0) t idc) (@eta_ident_cps_gen2 T0 f0 T1 f1 t idc).
- Proof. intros t idc; cbv [proj1_sig eta_ident_cps_gen eta_ident_cps_gen2]; destruct idc; exact (f2 _ _). Defined.
+ : { f' : forall t idc, T2 t idc (proj1_sig (@eta_ident_cps_gen T0 f0) t idc) (proj1_sig (@eta_ident_cps_gen2 T0 f0 T1 f1) t idc)
+ | forall t idc,
+ f' t idc
+ = rew [T2 t idc _] (eq_sym (proj2_sig (@eta_ident_cps_gen2 T0 f0 T1 f1) t idc)) in
+ match eq_sym (proj2_sig (@eta_ident_cps_gen _ f0) t idc) as p return T2 t idc _ (rew [T1 t idc] p in f1 t idc) with
+ | eq_refl => f2 t idc
+ end }.
+ Proof. apply eta_ident_cps_gen. Defined.
Module Raw.
Module ident.
Local Unset Decidable Equality Schemes.
+ Local Unset Boolean Equality Schemes.
Module MakeIdent.
Import Compilers.ident.
Ltac map_projT2 tac ls :=
@@ -401,6 +428,23 @@ Module Compilers.
Definition all_idents : list ident := ltac:(make_all_idents).
+ Definition ident_index : ident -> nat
+ := ltac:(let idc := fresh "idc" in
+ let idc' := fresh "idc'" in
+ let v := (eval cbv [id] in
+ (ltac:(intro idc;
+ pose idc as idc';
+ destruct idc;
+ let idc := (eval cbv [idc'] in idc') in
+ let all_idents := (eval cbv [all_idents] in all_idents) in
+ let n := get_ctor_number' idc all_idents in
+ exact n)
+ : ident -> nat)) in
+ refine v).
+
+ Lemma ident_index_idempotent idc : List.nth_error all_idents (ident_index idc) = Some idc.
+ Proof. destruct idc; vm_compute; reflexivity. Defined.
+
Definition eta_ident_cps_gen {T : ident -> Type}
(f : forall idc, T idc)
@@ -412,8 +456,10 @@ Module Compilers.
(f0 : forall idc, T0 idc)
{T1 : forall idc, T0 idc -> Type}
(f1 : forall idc, T1 idc (f0 idc))
- : forall idc, T1 idc (proj1_sig (@eta_ident_cps_gen T0 f0) idc).
- Proof. intros idc; cbv [proj1_sig eta_ident_cps_gen]; destruct idc; exact (f1 _). Defined.
+ : { f' : forall idc, T1 idc (proj1_sig (@eta_ident_cps_gen T0 f0) idc)
+ | forall idc,
+ f' idc = rew [T1 idc] (eq_sym (proj2_sig (@eta_ident_cps_gen T0 f0) idc)) in f1 idc }.
+ Proof. apply eta_ident_cps_gen. Defined.
Definition eta_ident_cps_gen3
{T0 : ident -> Type}
@@ -422,29 +468,85 @@ Module Compilers.
(f1 : forall idc, T1 idc (f0 idc))
{T2 : forall idc x, T1 idc x -> Type}
(f2 : forall idc, T2 idc (f0 idc) (f1 idc))
- : forall idc, T2 idc (proj1_sig (@eta_ident_cps_gen T0 f0) idc) (@eta_ident_cps_gen2 T0 f0 T1 f1 idc).
- Proof. intros idc; cbv [proj1_sig eta_ident_cps_gen eta_ident_cps_gen2]; destruct idc; exact (f2 _). Defined.
+ : { f' : forall idc, T2 idc (proj1_sig (@eta_ident_cps_gen T0 f0) idc) (proj1_sig (@eta_ident_cps_gen2 T0 f0 T1 f1) idc)
+ | forall idc,
+ f' idc
+ = rew [T2 idc _] (eq_sym (proj2_sig (@eta_ident_cps_gen2 T0 f0 T1 f1) idc)) in
+ match eq_sym (proj2_sig (@eta_ident_cps_gen _ f0) idc) as p return T2 idc _ (rew [T1 idc] p in f1 idc) with
+ | eq_refl => f2 idc
+ end }.
+ Proof. apply eta_ident_cps_gen. Defined.
+
+ Definition ident_beq : ident -> ident -> bool
+ := fun idc1 idc2
+ => proj1_sig
+ (eta_ident_cps_gen
+ (fun idc1
+ => proj1_sig
+ (eta_ident_cps_gen
+ (fun idc2
+ => Nat.eqb (ident_index idc1) (ident_index idc2)))
+ idc2))
+ idc1.
+
+ Ltac rew_proj2_sig :=
+ repeat match goal with
+ | [ |- context[@proj1_sig _ (fun _ => forall x, _ = _) ?p] ]
+ => rewrite !(proj2_sig p)
+ | [ |- context[@proj1_sig _ (fun _ => forall x y, _ = _) ?p] ]
+ => rewrite !(proj2_sig p)
+ end.
+
+ Definition nat_eqb_refl_transparent (x : nat) : Nat.eqb x x = true.
+ Proof. induction x; cbn; constructor + assumption. Defined.
Definition ident_lb (x y : ident) : x = y -> ident_beq x y = true.
- Proof. intro H; subst y; destruct x; reflexivity. Defined.
- Definition ident_beq_if (x y : ident) : if ident_beq x y then x = y else True.
- Proof. destruct x, y; cbv; constructor. Defined.
+ Proof.
+ intro H; subst y; cbv [ident_beq];
+ rew_proj2_sig; apply nat_eqb_refl_transparent.
+ Defined.
+
+ Lemma ident_index_inj idc1 idc2 : ident_index idc1 = ident_index idc2 -> idc1 = idc2.
+ Proof.
+ intro H.
+ pose proof (ident_index_idempotent idc1) as H1.
+ pose proof (ident_index_idempotent idc2) as H2.
+ rewrite H in H1; rewrite H1 in H2.
+ set (sidc1 := Some idc1) in *.
+ set (sidc2 := Some idc2) in *.
+ change (match sidc1, sidc2 with Some idc1, Some idc2 => idc1 = idc2 | _, _ => True end).
+ clearbody sidc2; subst sidc2 sidc1; reflexivity.
+ Defined.
+
+ Definition nat_eqb_bl_transparent (x y : nat) : Nat.eqb x y = true -> x = y.
+ Proof.
+ revert y; induction x, y; cbn; intro; try apply f_equal; auto using eq_refl with nocore;
+ exfalso; apply Bool.diff_false_true; assumption.
+ Defined.
+
Definition ident_bl (x y : ident) : ident_beq x y = true -> x = y.
Proof.
- generalize (ident_beq_if x y); destruct (ident_beq x y); intros;
- first [ assumption | exfalso; apply Bool.diff_false_true; assumption ].
+ cbv [ident_beq]; rew_proj2_sig; intro H.
+ apply nat_eqb_bl_transparent in H.
+ apply ident_index_inj in H.
+ exact H.
+ Defined.
+
+ Definition ident_beq_if (x y : ident) : if ident_beq x y then x = y else True.
+ Proof.
+ generalize (ident_beq x y), (ident_bl x y).
+ intros b H; destruct b; exact I + auto using eq_refl with nocore.
Defined.
Definition ident_transport_opt (P : ident -> Type) {x y : ident} : P x -> Datatypes.option (P y)
- := Eval cbv [ident_beq ident_beq_if] in
- fun v
- => (if ident_beq x y as b return (if b then x = y else True) -> _
- then fun pf => Datatypes.Some
- match pf in (_ = y) return P y with
- | eq_refl => v
- end
- else fun _ => Datatypes.None)
- (@ident_beq_if x y).
+ := fun v
+ => (if ident_beq x y as b return (if b then x = y else True) -> _
+ then fun pf => Datatypes.Some
+ match pf in (_ = y) return P y with
+ | eq_refl => v
+ end
+ else fun _ => Datatypes.None)
+ (@ident_beq_if x y).
Inductive kind_of_type := GallinaType (_ : Type) | BaseBaseType | BaseType.
Definition Type_of_kind_of_type (T : kind_of_type)
@@ -472,7 +574,10 @@ Module Compilers.
dep_types_dec_transparent : forall x y : type_of_list (dep_types preinfos), {x = y} + {x <> y};
indep_args_beq : _;
indep_args_reflect
- : forall x, reflect_rel (@eq (type_of_list (indep_args preinfos x))) (indep_args_beq x)
+ : forall x, reflect_rel (@eq (type_of_list (indep_args preinfos x))) (indep_args_beq x);
+ indep_types_beq : _;
+ indep_types_reflect
+ : reflect_rel (@eq (type_of_list_of_kind (indep_types preinfos))) indep_types_beq;
}.
Definition ident_args (pi : preident_infos)
@@ -481,25 +586,10 @@ Module Compilers.
Definition assemble_ident {pi} (args : ident_args pi)
:= to_ident pi (projT1 args) (Datatypes.fst (projT2 args)) (Datatypes.snd (projT2 args)).
- Ltac build_ident_to_cident :=
- let v
- := (eval cbv [proj1_sig eta_ident_cps_gen List.find List.combine all_idents pattern.all_idents ident_beq] in
- (fun default
- => proj1_sig
- (@eta_ident_cps_gen
- (fun _ => { T : Type & T })
- (fun idc
- => match List.find
- (fun '(idc', v) => ident_beq idc idc')
- (List.combine all_idents pattern.all_idents) with
- | Datatypes.Some (_, v) => v
- | Datatypes.None => default
- end)))) in
- let v := strip_default v in
- v.
- Ltac make_ident_to_cident := let v := build_ident_to_cident in refine v.
-
- Definition ident_to_cident : ident -> { T : Type & T } := ltac:(make_ident_to_cident).
+ Definition ident_to_cident : ident -> { T : Type & T }
+ := proj1_sig
+ (eta_ident_cps_gen
+ (fun idc => List.nth_default (@existT Type _ True I) pattern.all_idents (ident_index idc))).
Ltac fun_to_curried_ident_infos f :=
let type_to_kind T
@@ -555,12 +645,13 @@ Module Compilers.
| T
=> ltac:(destruct idc;
let T := (eval cbv [T ident_to_cident projT2] in (projT2 T)) in
+ let T := (eval cbv in T) in
let v := fun_to_curried_ident_infos T in
let v := (eval cbv [type_of_list List.map Type_of_kind_of_type] in v) in
let c := constr:(@Build_ident_infos v) in
let T := type of c in
let T := (eval cbv [dep_types indep_types indep_args type_of_list List.map Type_of_kind_of_type] in T) in
- refine ((c : T) _ _ _);
+ refine ((c : T) _ _ _ _ _);
repeat decide equality)
end) in
let v := (eval cbv [dep_types indep_types indep_args type_of_list preinfos List.map Type_of_kind_of_type Datatypes.prod_rect base.type.base_rect unit_rect sumbool_rect prod_rec unit_rec sumbool_rec base.type.base_rec eq_ind_r eq_ind eq_sym eq_rec eq_rect] in v) in
@@ -608,76 +699,99 @@ Module Compilers.
(exists ridc);
cbv [ident_infos_of ident_args type_of_list indep_args dep_types indep_types preinfos assemble_ident to_ident List.map Type_of_kind_of_type];
unshelve (eexists; refine_sigT_and_pair; try constructor);
- repeat esplit)
+ cbv [to_type Datatypes.fst];
+ try solve [ repeat unshelve esplit ])
: { ridc : ident & { args : ident_args (ident_infos_of ridc)
- | JMeq idc (assemble_ident args) } })) in
+ | { pf : _ = _
+ | idc = rew [Compilers.ident.ident] pf in assemble_ident args } } })) in
v.
Ltac make_split_ident_gen := let v := build_split_ident_gen in refine v.
Definition split_ident_gen
: forall {t} (idc : Compilers.ident.ident t),
{ ridc : ident & { args : ident_args (ident_infos_of ridc)
- | JMeq idc (assemble_ident args) } }
+ | { pf : _ = _
+ | idc = rew [Compilers.ident.ident] pf in assemble_ident args } } }
:= ltac:(make_split_ident_gen).
- Ltac do_reduce v :=
- let v := (eval cbv [proj1_sig eta_ident_cps_gen eta_ident_cps_gen2 eta_ident_cps_gen3 ident_args ident_infos_of type_of_list dep_types indep_types indep_args preinfos to_type ident_transport_opt split_ident_gen pattern.eta_ident_cps_gen to_ident to_type List.map Type_of_kind_of_type] in v) in
- v.
-
+ Definition prefull_types : ident -> Type
+ := fun idc => ident_args (ident_infos_of idc).
Definition full_types : ident -> Type
- := ltac:(let v := do_reduce
- (proj1_sig
- (eta_ident_cps_gen
- (fun idc
- => ident_args (ident_infos_of idc)))) in
- refine v).
+ := proj1_sig (eta_ident_cps_gen prefull_types).
Definition is_simple : ident -> bool
- := ltac:(let v := do_reduce
- (proj1_sig
- (eta_ident_cps_gen
- (fun idc
- => let ii := ident_infos_of idc in
- match dep_types ii, indep_types ii return _ with (* COQBUG(https://github.com/coq/coq/issues/9955) *)
- | [], [] => true
- | _, _ => false
- end))) in
- refine v).
+ := fun idc
+ => let ii := ident_infos_of idc in
+ match dep_types ii, indep_types ii return _ with (* COQBUG(https://github.com/coq/coq/issues/9955) *)
+ | [], [] => true
+ | _, _ => false
+ end.
Definition type_of : forall (pidc : ident), full_types pidc -> Compilers.type Compilers.base.type
- := ltac:(let v := do_reduce
- (@eta_ident_cps_gen2
- _ (fun idc => ident_args (ident_infos_of idc))
- (fun pidc full_types_pidc
- => full_types_pidc -> Compilers.type Compilers.base.type)
- (fun pidc args
- => to_type (ident_infos_of pidc) (projT1 args) (Datatypes.fst (projT2 args)))) in
- refine v).
+ := proj1_sig
+ (@eta_ident_cps_gen2
+ _ prefull_types
+ (fun pidc full_types_pidc => full_types_pidc -> Compilers.type Compilers.base.type)
+ (fun pidc args
+ => to_type (ident_infos_of pidc) (projT1 args) (Datatypes.fst (projT2 args)))).
+
+ Definition folded_invert_bind_args : forall {t} (idc : Compilers.ident.ident t) (pidc : ident), Datatypes.option (full_types pidc)
+ := fun t idc pidc
+ => proj1_sig
+ (pattern.eta_ident_cps_gen
+ (fun t idc
+ => proj1_sig
+ (@eta_ident_cps_gen2
+ _ prefull_types
+ (fun pidc full_types_pidc => Datatypes.option full_types_pidc)
+ (fun pidc
+ => let '(existT ridc (exist args _)) := split_ident_gen idc in
+ ident_transport_opt
+ (fun idc => ident_args (ident_infos_of idc))
+ args))
+ pidc))
+ t idc.
Definition invert_bind_args : forall {t} (idc : Compilers.ident.ident t) (pidc : ident), Datatypes.option (full_types pidc)
- := ltac:(let v := do_reduce
- (fun t idc pidc
- => proj1_sig
- (pattern.eta_ident_cps_gen
- (fun t idc
- => @eta_ident_cps_gen2
- _ (fun idc => ident_args (ident_infos_of idc))
- (fun pidc full_types_pidc => Datatypes.option full_types_pidc)
- (fun pidc
- => let '(existT ridc (exist args _)) := split_ident_gen idc in
- ident_transport_opt
- (fun idc => ident_args (ident_infos_of idc))
- args)
- pidc))
- t idc) in
+ := ltac:(let v := (eval cbv [folded_invert_bind_args] in (@folded_invert_bind_args)) in
+ let v := (eval cbv [pattern.eta_ident_cps_gen proj1_sig eta_ident_cps_gen2 eta_ident_cps_gen proj1_sig proj2_sig eq_rect eq_sym split_ident_gen projT2 ident_transport_opt ident_beq ident_index Nat.eqb ident_beq_if ident_bl eq_ind_r eq_ind nat_eqb_bl_transparent nat_ind ident_index_inj ident_index_idempotent f_equal] in v) in
refine v).
+
Definition to_typed : forall (pidc : ident) (args : full_types pidc), Compilers.ident.ident (type_of pidc args)
- := ltac:(let v := do_reduce
- (@eta_ident_cps_gen3
- _ (fun idc => ident_args (ident_infos_of idc))
- (fun pidc full_types_pidc => full_types_pidc -> Compilers.type Compilers.base.type)
- (fun pidc args => to_type (ident_infos_of pidc) (projT1 args) (Datatypes.fst (projT2 args)))
- (fun pidc full_types_pidc type_of_pidc => forall args : full_types_pidc, Compilers.ident.ident (type_of_pidc args))
- (fun pidc args
- => to_ident _ _ _ (Datatypes.snd (projT2 args)))) in
- refine v).
+ := proj1_sig
+ (@eta_ident_cps_gen3
+ _ prefull_types
+ (fun pidc full_types_pidc => full_types_pidc -> Compilers.type Compilers.base.type)
+ (fun pidc args => to_type (ident_infos_of pidc) (projT1 args) (Datatypes.fst (projT2 args)))
+ (fun pidc full_types_pidc type_of_pidc => forall args : full_types_pidc, Compilers.ident.ident (type_of_pidc args))
+ (fun pidc args
+ => to_ident _ _ _ (Datatypes.snd (projT2 args)))).
+
+ Definition try_unify_split_args {ridc1 ridc2 : ident}
+ : forall {dt1 : type_of_list (dep_types (preinfos (ident_infos_of ridc1)))}
+ {dt2 : type_of_list (dep_types (preinfos (ident_infos_of ridc2)))}
+ (*(idt1 : type_of_list_of_kind (indep_types (preinfos (ident_infos_of ridc1))))
+ (idt2 : type_of_list_of_kind (indep_types (preinfos (ident_infos_of ridc2))))*),
+ type_of_list (indep_args _ dt1) -> Datatypes.option (type_of_list (indep_args _ dt2))
+ := (if ident_beq ridc1 ridc2 as b return (if b then ridc1 = ridc2 else True) -> _
+ then fun pf
+ => match pf in (_ = ridc2) return forall (dt1 : type_of_list (dep_types (preinfos (ident_infos_of ridc1))))
+ (dt2 : type_of_list (dep_types (preinfos (ident_infos_of ridc2))))
+ (*(idt1 : type_of_list_of_kind (indep_types (preinfos (ident_infos_of ridc1))))
+ (idt2 : type_of_list_of_kind (indep_types (preinfos (ident_infos_of ridc2))))*),
+ type_of_list (indep_args _ dt1) -> Datatypes.option (type_of_list (indep_args _ dt2)) with
+ | eq_refl
+ => fun dt1 dt2 (*idt1 idt2*)
+ => match dep_types_dec_transparent _ dt1 dt2 with
+ | left pf
+ => match pf in (_ = dt2) return type_of_list (indep_args _ dt1) -> Datatypes.option (type_of_list (indep_args _ dt2)) with
+ | eq_refl
+ => (*if indep_types_beq _ idt1 idt2
+ then*) Datatypes.Some
+ (*else fun _ => Datatypes.None*)
+ end
+ | right _ => fun _ => Datatypes.None
+ end
+ end
+ else fun _ _ _ _ (*_ _*) => Datatypes.None)
+ (ident_beq_if ridc1 ridc2).
End ident.
Notation ident := ident.ident.
End Raw.
@@ -861,18 +975,26 @@ Module Compilers.
(f0 : forall t idc, T0 t idc)
{T1 : forall t (idc : ident t), T0 t idc -> Type}
(f1 : forall t idc, T1 t idc (f0 t idc))
- : forall t idc, T1 t idc (proj1_sig (@eta_ident_cps_gen T0 f0) t idc).
- Proof. intros t idc; cbv [proj1_sig eta_ident_cps_gen]; destruct idc; exact (f1 _ _). Defined.
+ : { f' : forall t idc, T1 t idc (proj1_sig (@eta_ident_cps_gen T0 f0) t idc)
+ | forall t idc,
+ f' t idc = rew [T1 t idc] (eq_sym (proj2_sig (@eta_ident_cps_gen T0 f0) t idc)) in f1 t idc }.
+ Proof. apply eta_ident_cps_gen. Defined.
Definition eta_ident_cps_gen3
{T0 : forall t, ident t -> Type}
(f0 : forall t idc, T0 t idc)
- {T1 : forall t (idc : ident t), T0 t idc -> Type}
+ {T1 : forall t idc, T0 t idc -> Type}
(f1 : forall t idc, T1 t idc (f0 t idc))
{T2 : forall t idc x, T1 t idc x -> Type}
(f2 : forall t idc, T2 t idc (f0 t idc) (f1 t idc))
- : forall t idc, T2 t idc (proj1_sig (@eta_ident_cps_gen T0 f0) t idc) (@eta_ident_cps_gen2 T0 f0 T1 f1 t idc).
- Proof. intros t idc; cbv [proj1_sig eta_ident_cps_gen eta_ident_cps_gen2]; destruct idc; exact (f2 _ _). Defined.
+ : { f' : forall t idc, T2 t idc (proj1_sig (@eta_ident_cps_gen T0 f0) t idc) (proj1_sig (@eta_ident_cps_gen2 T0 f0 T1 f1) t idc)
+ | forall t idc,
+ f' t idc
+ = rew [T2 t idc _] (eq_sym (proj2_sig (@eta_ident_cps_gen2 T0 f0 T1 f1) t idc)) in
+ match eq_sym (proj2_sig (@eta_ident_cps_gen _ f0) t idc) as p return T2 t idc _ (rew [T1 t idc] p in f1 t idc) with
+ | eq_refl => f2 t idc
+ end }.
+ Proof. apply eta_ident_cps_gen. Defined.
Definition Type_of_kind_of_type (T : Raw.ident.kind_of_type)
:= match T with
@@ -881,6 +1003,9 @@ Module Compilers.
| Raw.ident.BaseType => pattern.base.type.type
end.
+ Notation full_type_of_list_of_kind ls
+ := (type_of_list (List.map Raw.ident.Type_of_kind_of_type ls)).
+
Notation type_of_list_of_kind ls
:= (type_of_list (List.map Type_of_kind_of_type ls)).
@@ -980,176 +1105,198 @@ Module Compilers.
{ t : _ & { idc : ident t | @split_types _ idc = existT _ ridc (dt, idt) } }
:= ltac:(make_add_types_from_raw_sig (@split_types)).
+
+ Definition split_types_subst_default : forall {t} (idc : ident t) (evm : EvarMap), { ridc : Raw.ident & type_of_list (dep_types (preinfos (ident_infos_of ridc))) * full_type_of_list_of_kind (indep_types (preinfos (ident_infos_of ridc))) }%type
+ := fun t idc evm
+ => let res := @split_types t idc in
+ existT _ (projT1 res) (Datatypes.fst (projT2 res),
+ lift_type_of_list_map (@subst_default_kind_of_type evm) (Datatypes.snd (projT2 res))).
+
+ Lemma to_type_split_types_subst_default_eq t idc evm
+ : Raw.ident.to_type
+ (preinfos (ident_infos_of (projT1 (@split_types_subst_default t idc evm))))
+ (Datatypes.fst (projT2 (split_types_subst_default idc evm)))
+ (Datatypes.snd (projT2 (split_types_subst_default idc evm)))
+ = type.subst_default t evm.
+ Proof.
+ destruct idc; cbv -[type.subst_default base.subst_default];
+ cbn [type.subst_default base.subst_default]; reflexivity.
+ Defined.
+
+ Lemma projT1_add_types_from_raw_sig_eq t idc
+ : projT1
+ (add_types_from_raw_sig
+ (projT1 (Raw.ident.split_ident_gen idc))
+ (projT1 (proj1_sig (projT2 (Raw.ident.split_ident_gen idc))))
+ (lift_type_of_list_map
+ (@relax_kind_of_type)
+ (Datatypes.fst (projT2 (proj1_sig (projT2 (@Raw.ident.split_ident_gen t idc)))))))
+ = type.relax t.
+ Proof.
+ destruct idc; cbv -[type.relax base.relax];
+ cbn [type.relax base.relax]; reflexivity.
+ Defined.
+
Definition prearg_types : forall {t} (idc : ident t), list Type
:= (fun t idc
=> let st := @split_types t idc in
let pi := preinfos (ident_infos_of (projT1 st)) in
indep_args pi (Datatypes.fst (projT2 st))).
- Definition try_unify_split_args {ridc1 ridc2 : Raw.ident.ident}
- : forall {dt1 : type_of_list (dep_types (preinfos (ident_infos_of ridc1)))}
- {dt2 : type_of_list (dep_types (preinfos (ident_infos_of ridc2)))},
- type_of_list (indep_args _ dt1) -> Datatypes.option (type_of_list (indep_args _ dt2))
- := (if Raw.ident.ident_beq ridc1 ridc2 as b return (if b then ridc1 = ridc2 else True) -> _
- then fun pf
- => match pf in (_ = ridc2) return forall (dt1 : type_of_list (dep_types (preinfos (ident_infos_of ridc1))))
- (dt2 : type_of_list (dep_types (preinfos (ident_infos_of ridc2)))),
- type_of_list (indep_args _ dt1) -> Datatypes.option (type_of_list (indep_args _ dt2)) with
- | eq_refl
- => fun dt1 dt2
- => match Raw.ident.dep_types_dec_transparent _ dt1 dt2 with
- | left pf
- => match pf in (_ = dt2) return type_of_list (indep_args _ dt1) -> Datatypes.option (type_of_list (indep_args _ dt2)) with
- | eq_refl => Datatypes.Some
- end
- | right _ => fun _ => Datatypes.None
- end
- end
- else fun _ _ _ _ => Datatypes.None)
- (Raw.ident.ident_beq_if ridc1 ridc2).
-
- Ltac do_reduce v :=
- let v := (eval cbv [proj1_sig pattern.eta_ident_cps_gen pattern.eta_ident_cps_gen2 eta_ident_cps_gen eta_ident_cps_gen2 eta_ident_cps_gen3 eta_ident_cps_gen_expand_literal pattern.eta_ident_cps_gen_expand_literal split_types projT1 projT2 preinfos dep_types indep_types ident_infos_of split_types add_types_from_raw_sig type_of_list List.map List.app Type_of_kind_of_type indep_args lift_type_of_list_map relax_kind_of_type subst_default_kind_of_type Raw.ident.assemble_ident Raw.ident.to_type prearg_types Raw.ident.Type_of_kind_of_type Raw.ident.to_ident Raw.ident.indep_args_beq Raw.ident.split_ident_gen Raw.ident.dep_types_dec_transparent try_unify_split_args Raw.ident.ident_beq_if Raw.ident.dep_types_dec_transparent Raw.ident.ident_beq] in v) in
- let v := (eval cbn [Datatypes.fst Datatypes.snd] in v) in
- v.
-
Definition strip_types : forall {t} (idc : ident t), Raw.ident
- := ltac:(let v := do_reduce
- (proj1_sig
- (eta_ident_cps_gen
- (fun t idc => projT1 (@split_types t idc)))) in
- refine v).
+ := proj1_sig
+ (eta_ident_cps_gen
+ (fun t idc => projT1 (@split_types t idc))).
Definition arg_types : forall {t} (idc : ident t), list Type
- := ltac:(let v := (eval cbv [prearg_types] in (@prearg_types)) in
- let v := do_reduce
- (proj1_sig
- (eta_ident_cps_gen
- v)) in
- refine v).
- Definition to_typed : forall {t} (idc : ident t) (evm : EvarMap), type_of_list (arg_types idc) -> Compilers.ident.ident (pattern.type.subst_default t evm)
- := ltac:(let v := constr:
- (fun t (idc : ident t) (evm : EvarMap)
- => @eta_ident_cps_gen2
- _ (@prearg_types)
- (fun t idc arg_types_idc
- => forall args : type_of_list arg_types_idc,
- Compilers.ident.ident
- (let st := @split_types _ idc in
- let pi := preinfos (ident_infos_of (projT1 st)) in
- Raw.ident.to_type
- pi
- (Datatypes.fst (projT2 st))
- (lift_type_of_list_map
- (@subst_default_kind_of_type evm)
- (Datatypes.snd (projT2 st)))))
- (fun t idc args
- => let st := @split_types _ idc in
- (@Raw.ident.assemble_ident
- (preinfos (ident_infos_of (projT1 (@split_types _ idc))))
- (existT
- _ (Datatypes.fst (projT2 st))
- (lift_type_of_list_map (@subst_default_kind_of_type evm) (Datatypes.snd (projT2 st)), args))))
- t idc) in
- let V' := fresh "V'" in
- let v := constr:(
- (fun t (idc : ident t) (evm : EvarMap)
- => match v t idc evm return type_of_list (@arg_types _ idc) -> Compilers.ident.ident (pattern.type.subst_default t evm) with
- | V'
- => ltac:(destruct idc;
- let v := (eval cbv [V'] in V') in
- clear V';
- let v := do_reduce v in
- refine v)
- end)) in
- let v := (eval cbv [id] in v) in
- refine v).
+ := proj1_sig (eta_ident_cps_gen (@prearg_types)).
+
+ Definition arg_types_unfolded : forall {t} (idc : ident t), list Type
+ := Eval cbv -[base.interp] in @arg_types.
+
+ Definition to_typed : forall {t} (idc : ident t) (evm : EvarMap), type_of_list (arg_types idc) -> Compilers.ident.ident (type.subst_default t evm)
+ := fun t (idc : ident t) (evm : EvarMap)
+ => proj1_sig
+ (@eta_ident_cps_gen2
+ _ (@prearg_types)
+ (fun t idc arg_types_idc
+ => forall args : type_of_list arg_types_idc,
+ Compilers.ident.ident (type.subst_default t evm)
+ (*let st := @split_types _ idc in
+ let pi := preinfos (ident_infos_of (projT1 st)) in
+ Raw.ident.to_type
+ pi
+ (Datatypes.fst (projT2 st))
+ (lift_type_of_list_map
+ (@subst_default_kind_of_type evm)
+ (Datatypes.snd (projT2 st)))*))
+ (fun t idc args
+ => rew [Compilers.ident.ident] to_type_split_types_subst_default_eq t idc evm in
+ let st := @split_types_subst_default _ idc evm in
+ (@Raw.ident.assemble_ident
+ (preinfos (ident_infos_of (projT1 (@split_types_subst_default _ idc evm))))
+ (existT
+ _ (Datatypes.fst (projT2 st))
+ (Datatypes.snd (projT2 st), args)))))
+ t idc.
+
+ Definition to_typed_unfolded : forall {t} (idc : ident t) (evm : EvarMap), type_of_list (arg_types_unfolded idc) -> Compilers.ident.ident (type.subst_default t evm)
+ := ltac:(let v := (eval cbv -[type.subst_default base.subst_default arg_types_unfolded type_of_list base.base_interp Datatypes.fst Datatypes.snd] in
+ (fun t (idc : ident t) (evm : EvarMap)
+ => proj1_sig
+ (@eta_ident_cps_gen
+ (fun t idc => type_of_list (arg_types_unfolded idc) -> Compilers.ident.ident (type.subst_default t evm))
+ (fun t idc => @to_typed t idc evm))
+ t idc)) in
+ let v := (eval cbn [Datatypes.fst Datatypes.snd type_of_list] in v) in
+ exact v).
+
Definition type_of_list_arg_types_beq : forall t idc, type_of_list (@arg_types t idc) -> type_of_list (@arg_types t idc) -> bool
- := ltac:(let v := do_reduce
- (@eta_ident_cps_gen2
- _ (@prearg_types)
- (fun t idc arg_types_idc => type_of_list arg_types_idc -> type_of_list arg_types_idc -> bool)
- (fun t idc
- => Raw.ident.indep_args_beq _ _)) in
- refine v).
+ := proj1_sig
+ (@eta_ident_cps_gen2
+ _ (@prearg_types)
+ (fun t idc arg_types_idc => type_of_list arg_types_idc -> type_of_list arg_types_idc -> bool)
+ (fun t idc
+ => Raw.ident.indep_args_beq _ _)).
+
+ Definition type_of_list_arg_types_beq_unfolded : forall t idc, type_of_list (@arg_types_unfolded t idc) -> type_of_list (@arg_types_unfolded t idc) -> bool
+ := Eval cbv -[Prod.prod_beq arg_types_unfolded type_of_list base.interp_beq base.base_interp_beq Z.eqb base.base_interp ZRange.zrange_beq] in
+ proj1_sig
+ (@eta_ident_cps_gen
+ (fun t idc => type_of_list (@arg_types_unfolded t idc) -> type_of_list (@arg_types_unfolded t idc) -> bool)
+ (@type_of_list_arg_types_beq)).
+
Definition reflect_type_of_list_arg_types_beq : forall {t idc}, reflect_rel (@eq (type_of_list (@arg_types t idc))) (@type_of_list_arg_types_beq t idc)
- := @eta_ident_cps_gen3
- _ (@prearg_types)
- (fun t idc arg_types_idc => type_of_list arg_types_idc -> type_of_list arg_types_idc -> bool)
- (fun t idc => Raw.ident.indep_args_beq _ _)
- (fun t idc arg_types_idc beq => reflect_rel (@eq (type_of_list arg_types_idc)) beq)
- (fun t idc => Raw.ident.indep_args_reflect _ _).
- Definition preof_typed_ident
- := (fun t (idc : Compilers.ident.ident t)
- => proj1_sig
+ := proj1_sig
+ (@eta_ident_cps_gen3
+ _ (@prearg_types)
+ (fun t idc arg_types_idc => type_of_list arg_types_idc -> type_of_list arg_types_idc -> bool)
+ (fun t idc => Raw.ident.indep_args_beq _ _)
+ (fun t idc arg_types_idc beq => reflect_rel (@eq (type_of_list arg_types_idc)) beq)
+ (fun t idc => Raw.ident.indep_args_reflect _ _)).
+
+ Definition preof_typed_ident_sig : forall {t} (idc : Compilers.ident.ident t), _
+ := fun t idc
+ => add_types_from_raw_sig
+ (projT1 (Raw.ident.split_ident_gen idc))
+ (projT1 (proj1_sig (projT2 (Raw.ident.split_ident_gen idc))))
+ (lift_type_of_list_map
+ (@relax_kind_of_type)
+ (Datatypes.fst (projT2 (proj1_sig (projT2 (Raw.ident.split_ident_gen idc)))))).
+ Definition preof_typed_ident : forall {t} (idc : Compilers.ident.ident t), ident (type.relax t)
+ := fun t idc
+ => rew [ident] projT1_add_types_from_raw_sig_eq t idc in
+ proj1_sig
(projT2
- (add_types_from_raw_sig
- (projT1 (Raw.ident.split_ident_gen idc))
- (projT1 (proj1_sig (projT2 (Raw.ident.split_ident_gen idc))))
- (lift_type_of_list_map
- (@relax_kind_of_type)
- (Datatypes.fst (projT2 (proj1_sig (projT2 (Raw.ident.split_ident_gen idc))))))))).
+ (@preof_typed_ident_sig t idc)).
Definition of_typed_ident : forall {t} (idc : Compilers.ident.ident t), ident (type.relax t)
- := ltac:(let v := (eval cbv [preof_typed_ident] in
+ := proj1_sig (pattern.eta_ident_cps_gen (@preof_typed_ident)).
+
+ Definition of_typed_ident_unfolded : forall {t} (idc : Compilers.ident.ident t), ident (type.relax t)
+ := ltac:(let v := (eval cbv -[type.relax base.relax] in @of_typed_ident) in
+ let v := (eval cbn [type.relax base.relax] in v) in
+ exact v).
+
+ Definition arg_types_of_typed_ident : forall {t} (idc : Compilers.ident.ident t), type_of_list (arg_types (of_typed_ident idc)).
+ Proof.
+ refine (proj1_sig
+ (@pattern.eta_ident_cps_gen2
+ _ (@preof_typed_ident)
+ (fun t idc of_typed_ident_idc => type_of_list (arg_types of_typed_ident_idc))
+ (fun t idc
+ => match projT1_add_types_from_raw_sig_eq t idc as H'
+ return type_of_list (arg_types (rew [ident] H' in proj1_sig (projT2 (@preof_typed_ident_sig _ idc))))
+ with
+ | eq_refl
+ => rew <- [type_of_list]
+ (proj2_sig (eta_ident_cps_gen (@prearg_types))
+ (projT1 (preof_typed_ident_sig idc))
+ (proj1_sig (projT2 (preof_typed_ident_sig idc)))) in
+ rew <- [fun k' => type_of_list (indep_args (preinfos (ident_infos_of (projT1 k'))) (Datatypes.fst (projT2 k')))]
+ (proj2_sig (projT2 (@preof_typed_ident_sig t idc))) in
+ _
+ end))).
+ refine (let st := Raw.ident.split_ident_gen idc in
+ let args := proj1_sig (projT2 st) in
+ Datatypes.snd (projT2 args)).
+ Defined.
+
+ Definition arg_types_of_typed_ident_unfolded : forall {t} (idc : Compilers.ident.ident t), type_of_list (arg_types_unfolded (of_typed_ident_unfolded idc))
+ := ltac:(let v := (eval cbv -[type.relax base.relax type_of_list of_typed_ident arg_types_unfolded of_typed_ident_unfolded base.base_interp] in
(proj1_sig
- (pattern.eta_ident_cps_gen
- preof_typed_ident))) in
- let V' := fresh "V'" in
- let v := constr:(
- (fun t (idc : Compilers.ident.ident t)
- => match v t idc return ident (type.relax t) with
- | V'
- => ltac:(destruct idc;
- let v := (eval cbv [V'] in V') in
- clear V';
- let v := do_reduce v in
- refine v)
- end)) in
- let v := (eval cbv [id] in v) in
- refine v).
- Definition arg_types_of_typed_ident : forall {t} (idc : Compilers.ident.ident t), type_of_list (arg_types (of_typed_ident idc))
- := ltac:(let v := constr:(fun t (idc : Compilers.ident.ident t)
- => let st := Raw.ident.split_ident_gen idc in
- let args := proj1_sig (projT2 st) in
- Datatypes.snd (projT2 args)) in
- let V' := fresh "V'" in
- let v := constr:(
- (fun t (idc : Compilers.ident.ident t)
- => match v t idc return type_of_list (arg_types (of_typed_ident idc)) with
- | V'
- => ltac:(destruct idc;
- let v := (eval cbv [V'] in V') in
- clear V';
- let v := do_reduce v in
- refine v)
- end)) in
- let v := (eval cbv [id] in v) in
- refine v).
-
- Definition unify : forall {t t'} (pidc : ident t) (idc : Compilers.ident.ident t'), Datatypes.option (type_of_list (@arg_types t pidc))
- := ltac:(let v := constr:(fun t t' (pidc : ident t) (idc : Compilers.ident.ident t')
- => proj1_sig
- (eta_ident_cps_gen_expand_literal
- (fun t pidc
- => proj1_sig
- (pattern.eta_ident_cps_gen_expand_literal
- (fun t' idc
- => @eta_ident_cps_gen2
- _ (@prearg_types)
- (fun _ idc arg_types_idc => type_of_list arg_types_idc -> Datatypes.option (type_of_list (@arg_types t pidc)))
- (fun t idc
- => @eta_ident_cps_gen2
- _ (@prearg_types)
- (fun _ pidc arg_types_pidc => type_of_list (@prearg_types _ idc) -> Datatypes.option (type_of_list arg_types_pidc))
- (fun t' pidc
- => try_unify_split_args)
- _ pidc)
- _ (of_typed_ident idc) (@arg_types_of_typed_ident _ idc)))
- _ idc))
- _ pidc) in
- let v := (eval cbv [of_typed_ident arg_types_of_typed_ident] in v) in
- let v := (eval cbv [pattern.eta_ident_cps_gen_expand_literal proj1_sig eta_ident_cps_gen_expand_literal eta_ident_cps_gen2 split_types projT1 projT2 try_unify_split_args Raw.ident.ident_beq_if Raw.ident.dep_types_dec_transparent Raw.ident.ident_beq Raw.ident.dep_types_dec_transparent ident_infos_of Datatypes.fst Datatypes.snd] in v) in
- refine v).
-
+ (@pattern.eta_ident_cps_gen
+ (fun t idc => type_of_list (arg_types_unfolded (of_typed_ident_unfolded idc)))
+ (@arg_types_of_typed_ident)))) in
+ exact v).
+
+ Definition folded_unify : forall {t t'} (pidc : ident t) (idc : Compilers.ident.ident t') (*evm : EvarMap*), Datatypes.option (type_of_list (@arg_types t pidc))
+ := fun t t' (pidc : ident t) (idc : Compilers.ident.ident t') (*evm : EvarMap*)
+ => proj1_sig
+ (eta_ident_cps_gen_expand_literal
+ (fun t pidc
+ => proj1_sig
+ (pattern.eta_ident_cps_gen_expand_literal
+ (fun t' idc
+ => proj1_sig
+ (@eta_ident_cps_gen2
+ _ (@prearg_types)
+ (fun _ idc arg_types_idc => type_of_list arg_types_idc -> Datatypes.option (type_of_list (@arg_types t pidc)))
+ (fun t idc
+ => proj1_sig
+ (@eta_ident_cps_gen2
+ _ (@prearg_types)
+ (fun _ pidc arg_types_pidc => type_of_list (@prearg_types _ idc) -> Datatypes.option (type_of_list arg_types_pidc))
+ (fun t' pidc idc_indep_args
+ => Raw.ident.try_unify_split_args
+ (*(Datatypes.snd (projT2 (@split_types_subst_default _ idc evm)))
+ (Datatypes.snd (projT2 (@split_types_subst_default _ pidc evm)))*)
+ idc_indep_args))
+ _ pidc))
+ _ (of_typed_ident idc) (@arg_types_of_typed_ident _ idc)))
+ _ idc))
+ _ pidc.
+
+ Definition unify : forall {t t'} (pidc : ident t) (idc : Compilers.ident.ident t') (*evm : EvarMap*), Datatypes.option (type_of_list (@arg_types t pidc))
+ := Eval vm_compute in @folded_unify.
End ident.
End pattern.
End Compilers.
diff --git a/src/GENERATEDIdentifiersWithoutTypesProofs.v b/src/GENERATEDIdentifiersWithoutTypesProofs.v
index 2bab688dc..7c3ec0e35 100644
--- a/src/GENERATEDIdentifiersWithoutTypesProofs.v
+++ b/src/GENERATEDIdentifiersWithoutTypesProofs.v
@@ -1,6 +1,7 @@
Require Import Coq.ZArith.ZArith.
Require Import Coq.MSets.MSetPositive.
Require Import Coq.FSets.FMapPositive.
+Require Import Crypto.Util.PrimitiveSigma.
Require Import Crypto.Util.MSetPositive.Facts.
Require Import Crypto.Util.CPSNotations.
Require Import Crypto.Util.ZRange.
@@ -9,6 +10,8 @@ Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.Option.
Require Import Crypto.Util.Decidable.
Require Import Crypto.Util.HProp.
+Require Import Crypto.Util.Equality.
+Require Import Crypto.Util.Tactics.SpecializeBy.
Require Import Crypto.Language.
Require Import Crypto.LanguageInversion.
Require Import Crypto.GENERATEDIdentifiersWithoutTypes.
@@ -17,6 +20,7 @@ Require Import Crypto.Util.FixCoqMistakes.
Import EqNotations.
Module Compilers.
Import Language.Compilers.
+ Import LanguageInversion.Compilers.
Import GENERATEDIdentifiersWithoutTypes.Compilers.
Module pattern.
@@ -59,14 +63,24 @@ Module Compilers.
-> P v.
Proof. destruct v'; congruence. Qed.
+ Local Notation type_of_list := (List.fold_right (fun A B => prod A B) unit).
+ Fixpoint eta_type_of_list {ls} : type_of_list ls -> type_of_list ls
+ := match ls with
+ | nil => fun _ => tt
+ | cons x xs => fun v => (fst v, @eta_type_of_list xs (snd v))
+ end.
+ Lemma eq_eta_type_of_list ls v
+ : @eta_type_of_list ls v = v.
+ Proof. induction ls; destruct v; cbn; reflexivity + apply f_equal; auto with nocore. Defined.
+
Module base.
- Definition eq_subst_default_relax {t evm} : base.subst_default (base.relax t) evm = t.
+ Fixpoint eq_subst_default_relax {t evm} : base.subst_default (base.relax t) evm = t.
Proof.
- induction t; cbn;
+ destruct t; cbn;
first [ reflexivity
| apply f_equal
| apply f_equal2 ];
- assumption.
+ auto with nocore.
Defined.
End base.
@@ -79,6 +93,93 @@ Module Compilers.
Defined.
End type.
+ Local Lemma fast_sig_forall1_eq_ind {A T g}
+ (P : { f : forall a : A, T a | forall a, f a = g a } -> Type)
+ : (forall x : forall a, { f : T a | f = g a },
+ P (exist (fun f => forall a, f a = g a)
+ (fun a => proj1_sig (x a))
+ (fun a => proj2_sig (x a))))
+ -> forall x, P x.
+ Proof.
+ intros H [x p]; refine (H (fun a => exist _ (x a) (p a))).
+ Defined.
+
+ Local Lemma fast_sig_forall2_eq_ind {A B T g}
+ (P : { f : forall (a : A) (b : B a), T a b | forall a b, f a b = g a b } -> Type)
+ : (forall x : forall a b, { f : T a b | f = g a b },
+ P (exist (fun f => forall a b, f a b = g a b)
+ (fun a b => proj1_sig (x a b))
+ (fun a b => proj2_sig (x a b))))
+ -> forall x, P x.
+ Proof.
+ intros H [x p]; refine (H (fun a b => exist _ (x a b) (p a b))).
+ Defined.
+
+ Local Ltac my_generalize_dependent_intros v :=
+ let k := fresh in
+ set (k := v) in *; clearbody k.
+ Ltac my_prerevert_dependent H := (* apparently this is faster *)
+ move H at bottom;
+ repeat lazymatch goal with H' : _ |- _ => tryif constr_eq H H' then fail else revert H' end.
+ Local Ltac generalize_proj1_sig_step :=
+ match goal with
+ | [ |- context[@proj1_sig _ (fun x => forall y, _ = _) ?p] ]
+ => tryif is_var p then fail else my_generalize_dependent_intros p
+ | [ |- context[@proj1_sig _ (fun x => forall y z, _ = _) ?p] ]
+ => tryif is_var p then fail else my_generalize_dependent_intros p
+ | [ H : context[@proj1_sig _ (fun x => forall y, _ = _) ?p] |- _ ]
+ => tryif is_var p then fail else my_generalize_dependent_intros p
+ | [ H : context[@proj1_sig _ (fun x => forall y z, _ = _) ?p] |- _ ]
+ => tryif is_var p then fail else my_generalize_dependent_intros p
+ end.
+ Local Ltac specialize_sig_step :=
+ match goal with
+ | [ H : { f : forall (a : ?A), @?T a | forall a', f a' = @?g a' } |- _ ]
+ => my_prerevert_dependent H;
+ revert H;
+ let P := lazymatch goal with |- forall x, @?P x => P end in
+ refine (@fast_sig_forall1_eq_ind A T g P _);
+ cbn [proj1_sig proj2_sig]; intros
+ | [ H : { f : forall (a : ?A) (b : @?B a), @?T a b | forall a' b', f a' b' = @?g a' b' } |- _ ]
+ => my_prerevert_dependent H;
+ revert H;
+ let P := lazymatch goal with |- forall x, @?P x => P end in
+ refine (@fast_sig_forall2_eq_ind A B T g P _);
+ cbn [proj1_sig proj2_sig]; intros
+ end.
+ Local Ltac rewrite_sig_step :=
+ match goal with
+ | [ p : forall t idc, sig (fun y => y = _) |- _ ]
+ => lazymatch goal with
+ | [ H : context[proj1_sig (p ?t ?idc)] |- _ ] => destruct (p t idc)
+ | [ |- context[proj1_sig (p ?t ?idc)] ] => destruct (p t idc)
+ end;
+ subst; cbn [proj1_sig proj2_sig] in *; try clear p
+ | [ p : forall idc, sig (fun y => y = _) |- _ ]
+ => lazymatch goal with
+ | [ H : context[proj1_sig (p ?idc)] |- _ ] => destruct (p idc)
+ | [ |- context[proj1_sig (p ?idc)] ] => destruct (p idc)
+ end;
+ subst; cbn [proj1_sig proj2_sig] in *; try clear p
+ | [ p : sig (fun y => y = _) |- _ ]
+ => destruct p; subst; cbn [proj1_sig proj2_sig] in *
+ end.
+ Local Ltac clear_useless_step :=
+ match goal with
+ | [ H : forall t, { f : _ | f = _ } |- _ ] => clear H
+ | [ H : forall t idc, { f : _ | f = _ } |- _ ] => clear H
+ end.
+
+ Local Ltac do_rew_proj2_sig :=
+ repeat first [ progress cbn [eq_rect eq_sym] in *
+ | progress intros
+ | clear_useless_step
+ | rewrite_sig_step
+ | specialize_sig_step
+ | generalize_proj1_sig_step ].
+
+ Local Notation iffT x y := ((x -> y) * (y -> x))%type.
+
Module Raw.
Module ident.
Import GENERATEDIdentifiersWithoutTypes.Compilers.pattern.Raw.ident.
@@ -87,22 +188,106 @@ Module Compilers.
Global Instance eq_ident_Decidable : DecidableRel (@eq ident)
:= dec_rel_of_bool_dec_rel ident_beq ident_bl ident_lb.
+ Lemma is_simple_correct0 p
+ : is_simple p = true
+ <-> (forall f1 f2, type_of p f1 = type_of p f2).
+ Proof.
+ destruct p; cbn; cbv -[Datatypes.fst Datatypes.snd projT1 projT2] in *; split; intro H;
+ try solve [ reflexivity | exfalso; discriminate ].
+ all: repeat first [ match goal with
+ | [ H : nat -> ?A |- _ ] => specialize (H O)
+ | [ H : unit -> ?A |- _ ] => specialize (H tt)
+ | [ H : forall x y : PrimitiveProd.Primitive.prod _ _, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (PrimitiveProd.Primitive.pair x1 x2) (PrimitiveProd.Primitive.pair y1 y2)); cbn in H
+ | [ H : forall x y : Datatypes.prod _ _, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (Datatypes.pair x1 x2) (Datatypes.pair y1 y2)); cbn in H
+ | [ H : forall x y : PrimitiveSigma.Primitive.sigT ?P, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (PrimitiveSigma.Primitive.existT P x1 x2) (PrimitiveSigma.Primitive.existT P y1 y2)); cbn in H
+ | [ H : forall x y : Compilers.base.type, _ |- _ ] => specialize (fun x y => H (Compilers.base.type.type_base x) (Compilers.base.type.type_base y))
+ | [ H : forall x y : Compilers.base.type.base, _ |- _ ] => specialize (H Compilers.base.type.unit Compilers.base.type.nat); try congruence; cbn in H
+ end
+ | congruence ].
+ Qed.
+
+ Lemma invert_bind_args_to_typed p f
+ : invert_bind_args (to_typed p f) p = Some f.
+ Proof.
+ destruct p; cbv in *;
+ destruct_head' (@Primitive.sigT); destruct_head'_prod; destruct_head'_unit; reflexivity.
+ Qed.
+
+ Lemma fold_invert_bind_args : @invert_bind_args = @folded_invert_bind_args.
+ Proof. reflexivity. Qed.
+
+ Lemma split_ident_to_ident ridc x y z
+ : PrimitiveSigma.Primitive.projT1 (split_ident_gen (to_ident (ident_infos_of ridc) x y z))
+ = ridc.
+ Proof. destruct ridc; reflexivity. Defined.
+
+ Lemma eq_indep_types_of_eq_types (ridc : ident)
+ (dt1 dt2 : type_of_list (dep_types (ident_infos_of ridc)))
+ (idt1 idt2 : type_of_list_of_kind (indep_types (ident_infos_of ridc)))
+ (Hty : to_type (ident_infos_of ridc) dt1 idt1 = to_type (ident_infos_of ridc) dt2 idt2)
+ : idt1 = idt2.
+ Proof.
+ destruct ridc; cbv in *;
+ destruct_head'_prod; destruct_head'_unit; try reflexivity;
+ type.inversion_type; reflexivity.
+ Qed.
+
+ Lemma ident_transport_opt_correct P x y v
+ : (@ident_transport_opt P x y v <> None -> x = y)
+ * (forall pf : x = y, @ident_transport_opt P x y v = Some (rew pf in v)).
+ Proof.
+ cbv [ident_transport_opt].
+ generalize (ident_beq_if x y), (ident_lb x y); destruct (ident_beq x y);
+ intros; subst; split; try congruence; intros; subst;
+ try intuition congruence.
+ eliminate_hprop_eq; reflexivity.
+ Qed.
+
+ Lemma ident_transport_opt_correct' P x y v
+ : @ident_transport_opt P x y v <> None
+ -> { pf : x = y
+ | @ident_transport_opt P x y v = Some (rew pf in v) }.
+ Proof.
+ intro H; apply ident_transport_opt_correct in H; exists H; apply ident_transport_opt_correct.
+ Qed.
+
+ Lemma ident_transport_opt_correct'' P x y v v'
+ : @ident_transport_opt P x y v = Some v'
+ -> { pf : x = y
+ | v' = rew pf in v }.
+ Proof.
+ intro H.
+ pose proof (@ident_transport_opt_correct' P x y v) as H'.
+ rewrite H in H'.
+ specialize (H' ltac:(congruence)).
+ destruct H'; inversion_option; subst; (exists eq_refl); reflexivity.
+ Qed.
+
Lemma to_typed_invert_bind_args_gen t idc p f
: @invert_bind_args t idc p = Some f
-> { pf : t = type_of p f | @to_typed p f = rew [Compilers.ident.ident] pf in idc }.
Proof.
- cbv [invert_bind_args type_of full_types].
- repeat first [ reflexivity
- | (exists eq_refl)
- | progress intros
- | match goal with
- | [ H : Some _ = None |- ?P ] => exact (@quick_invert_eq_option _ P _ _ H)
- | [ H : None = Some _ |- ?P ] => exact (@quick_invert_eq_option _ P _ _ H)
- end
- | progress inversion_option
- | progress subst
- | break_innermost_match_step
- | break_innermost_match_hyps_step ].
+ rewrite fold_invert_bind_args.
+ cbv [folded_invert_bind_args type_of full_types to_typed] in *.
+ do_rew_proj2_sig.
+ all: repeat first [ match goal with
+ | [ |- context[@split_ident_gen ?t ?idc] ]
+ => destruct (@split_ident_gen t idc)
+ | [ H : context[@split_ident_gen ?t ?idc] |- _ ]
+ => destruct (@split_ident_gen t idc)
+ | [ H : Some _ = @ident_transport_opt _ _ _ _ |- _ ] => symmetry in H
+ | [ H : None = @ident_transport_opt _ _ _ _ |- _ ] => symmetry in H
+ | [ H : @ident_transport_opt ?P ?x ?y ?v = Some _ |- _ ]
+ => apply (@ident_transport_opt_correct'' P x y v) in H; destruct H
+ | [ H : @ident_transport_opt ?P ?x ?y ?v = None |- _ ]
+ => repeat intro; unshelve (erewrite (Datatypes.snd (ident_transport_opt_correct P x y v)) in H; inversion_option); []
+ end
+ | progress destruct_head'_sig
+ | progress subst
+ | progress cbv [eq_rect assemble_ident] in *
+ | (exists eq_refl)
+ | reflexivity
+ | break_innermost_match_step ].
Qed.
Lemma type_of_invert_bind_args t idc p f
@@ -117,33 +302,6 @@ Module Compilers.
exact (proj2_sig (@to_typed_invert_bind_args_gen t idc p f pf)).
Defined.
- Lemma invert_bind_args_to_typed p f
- : invert_bind_args (to_typed p f) p = Some f.
- Proof.
- destruct p; cbn in *;
- repeat first [ reflexivity
- | progress destruct_head'_unit
- | progress destruct_head'_prod
- | progress destruct_head' (@PrimitiveSigma.Primitive.sigT) ].
- Qed.
-
- Lemma is_simple_correct0 p
- : is_simple p = true
- <-> (forall f1 f2, type_of p f1 = type_of p f2).
- Proof.
- destruct p; cbn; split; intro H;
- try solve [ reflexivity | exfalso; discriminate ].
- all: repeat first [ match goal with
- | [ H : nat -> ?A |- _ ] => specialize (H O)
- | [ H : unit -> ?A |- _ ] => specialize (H tt)
- | [ H : forall x y : Datatypes.prod _ _, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (Datatypes.pair x1 x2) (Datatypes.pair y1 y2)); cbn in H
- | [ H : forall x y : PrimitiveSigma.Primitive.sigT ?P, _ |- _ ] => specialize (fun x1 y1 x2 y2 => H (PrimitiveSigma.Primitive.existT P x1 x2) (PrimitiveSigma.Primitive.existT P y1 y2)); cbn in H
- | [ H : forall x y : Compilers.base.type, _ |- _ ] => specialize (fun x y => H (Compilers.base.type.type_base x) (Compilers.base.type.type_base y))
- | [ H : forall x y : Compilers.base.type.base, _ |- _ ] => specialize (H Compilers.base.type.unit Compilers.base.type.nat); try congruence; cbn in H
- end
- | congruence ].
- Qed.
-
Lemma is_simple_correct p
: is_simple p = true
<-> (forall t1 idc1 t2 idc2, @invert_bind_args t1 idc1 p <> None -> @invert_bind_args t2 idc2 p <> None -> t1 = t2).
@@ -157,6 +315,64 @@ Module Compilers.
apply (H _ (to_typed p f1) _ (to_typed p f2));
rewrite invert_bind_args_to_typed; congruence. }
Qed.
+
+ Lemma try_unify_split_args_Some_correct ridc1 ridc2 dt1 dt2 (*idt1 idt2*) args v
+ : iffT
+ (@try_unify_split_args ridc1 ridc2 dt1 dt2 (*idt1 idt2*) args = Some v)
+ { pf : existT _ ridc1 dt1 = existT _ ridc2 dt2 :> { ridc : _ & type_of_list (dep_types (preinfos (ident_infos_of ridc))) }
+ | (rew [fun rdt => type_of_list (indep_args _ (projT2 rdt))] pf in
+ (args : type_of_list (indep_args _ (projT2 (existT _ ridc1 dt1)))))
+ = v
+ (*/\ (rew [fun ridc => type_of_list_of_kind (indep_types (preinfos (ident_infos_of ridc)))] f_equal (@projT1 _ _) pf in
+ idt1)
+ = idt2*) }.
+ Proof.
+ pose proof (dep_types_dec_transparent (ident_infos_of ridc1) : DecidableRel eq).
+ cbv [try_unify_split_args].
+ generalize (Raw.ident.ident_beq_if ridc1 ridc2).
+ generalize (Raw.ident.ident_lb ridc1 ridc2).
+ destruct (Raw.ident.ident_beq ridc1 ridc2);
+ [
+ | split;
+ [ congruence
+ | intros; destruct_head'_sig; Sigma.inversion_sigma; subst; specialize_by reflexivity; congruence ] ].
+ intros ? ?; subst.
+ (*pose proof (@Reflect.reflect_bool _ _ (indep_types_reflect _ idt1 idt2)) as H'.
+ pose proof (indep_types_reflect _ idt1 idt2) as H''.*)
+ repeat first [ break_innermost_match_step
+ | apply pair
+ | progress intros
+ | progress inversion_option
+ | progress subst
+ | progress specialize_by reflexivity
+ | apply conj
+ | progress destruct_head'_and
+ | progress destruct_head'_sig
+ | progress Sigma.inversion_sigma
+ | progress cbn [eq_rect eq_sym eq_rect_r Sigma.path_sigT Sigma.path_sigT_uncurried f_equal] in *
+ | (exists eq_refl)
+ | reflexivity
+ | progress eliminate_hprop_eq
+ | match goal with
+ | [ H : Bool.reflect _ false |- _ ] => inversion H; clear H
+ end
+ | congruence ].
+ Qed.
+
+ Lemma try_unify_split_args_None_correct ridc1 ridc2 dt1 dt2 (*idt1 idt2*) args
+ : @try_unify_split_args ridc1 ridc2 dt1 dt2 (*idt1 idt2*) args = None
+ -> forall pf : existT _ ridc1 dt1 = existT _ ridc2 dt2 :> { ridc : _ & type_of_list (dep_types (preinfos (ident_infos_of ridc))) },
+ (*(rew [fun ridc => type_of_list_of_kind (indep_types (preinfos (ident_infos_of ridc)))] f_equal (@projT1 _ _) pf in
+ idt1)
+ = idt2
+ ->*) False.
+ Proof.
+ intros H pf (*pf'*).
+ pose proof (fun v => snd (@try_unify_split_args_Some_correct ridc1 ridc2 dt1 dt2 (*idt1 idt2*) args v)) as H'.
+ rewrite H in H'.
+ specialize (H' _ (exist _ pf eq_refl(*(conj eq_refl pf')*))); cbv beta in *.
+ congruence.
+ Qed.
End ident.
End Raw.
@@ -164,30 +380,180 @@ Module Compilers.
Import GENERATEDIdentifiersWithoutTypes.Compilers.pattern.ident.
Import Datatypes. (* for Some, None, option *)
+ Lemma fold_eta_ident_cps T t idc f : @eta_ident_cps T t idc f = proj1_sig (@pattern.eta_ident_cps_gen (fun t _ => T t) f) t idc.
+ Proof. reflexivity. Qed.
+
+ Lemma fold_unify : @unify = @folded_unify.
+ Proof. vm_cast_no_check (eq_refl (@unify)). Qed.
+
+ Lemma to_typed_of_typed_ident t idc evm
+ : (rew [Compilers.ident] type.eq_subst_default_relax in
+ @to_typed _ (@of_typed_ident t idc) evm (@arg_types_of_typed_ident t idc))
+ = idc.
+ Proof.
+ destruct idc;
+ try (vm_compute; reflexivity);
+ cbv -[type.type_ind type.relax type.subst_default Compilers.base.type.type_ind f_equal f_equal2 base.relax base.subst_default base.eq_subst_default_relax];
+ cbn [type.type_ind type.relax type.subst_default f_equal f_equal2 base.relax base.subst_default base.eq_subst_default_relax];
+ repeat first [ progress subst
+ | progress intros
+ | progress cbn [f_equal f_equal2]
+ | reflexivity
+ | match goal with
+ | [ |- context[@base.eq_subst_default_relax ?t ?evm] ]
+ => generalize (base.subst_default (base.relax t) evm), (@base.eq_subst_default_relax t evm)
+ end ].
+ Qed.
+
+ Lemma eq_indep_types_of_eq_types {t1 t2} {idc1 : ident t1} {idc2 : ident t2} evm1 evm2
+ (Hty : type.subst_default t1 evm1 = type.subst_default t2 evm2)
+ (pf : Primitive.projT1 (@split_types_subst_default _ idc1 evm1)
+ = Primitive.projT1 (@split_types_subst_default _ idc2 evm2))
+ : Datatypes.snd (Primitive.projT2 (@split_types_subst_default _ idc1 evm1))
+ = rew <- [fun r => full_type_of_list_of_kind (Raw.ident.indep_types (Raw.ident.preinfos (Raw.ident.ident_infos_of r)))] pf in
+ Datatypes.snd (Primitive.projT2 (@split_types_subst_default _ idc2 evm2)).
+ Proof.
+ pose proof (@to_type_split_types_subst_default_eq _ idc1 evm1).
+ pose proof (@to_type_split_types_subst_default_eq _ idc2 evm2).
+ generalize dependent (type.subst_default t1 evm1);
+ generalize dependent (type.subst_default t2 evm2); intros; subst.
+ cbv [split_types_subst_default] in *; cbn [Primitive.projT1 Primitive.projT2 fst snd] in *.
+ destruct (split_types idc1), (split_types idc2);
+ destruct_head'_prod;
+ cbn [Primitive.projT1 Primitive.projT2 fst snd] in *;
+ subst; cbn [eq_rect eq_rect_r eq_sym].
+ eapply Raw.ident.eq_indep_types_of_eq_types; eassumption.
+ Qed.
+
Lemma eta_ident_cps_correct T t idc f
: @eta_ident_cps T t idc f = f t idc.
- Proof. cbv [eta_ident_cps]; break_innermost_match; reflexivity. Qed.
+ Proof. rewrite fold_eta_ident_cps; apply (proj2_sig (@pattern.eta_ident_cps_gen _ f)). Qed.
Lemma unify_to_typed {t t' pidc idc}
: forall v,
@unify t t' pidc idc = Some v
-> forall evm pf,
- rew [Compilers.ident] pf in @to_typed t pidc evm v = idc.
+ rew [Compilers.ident] pf in @to_typed t pidc evm v = idc.
Proof.
- refine (@option_case_fast _ _ _ _).
- Time destruct pidc, idc; cbv [unify to_typed]; try exact I.
- Time all: break_innermost_match; try exact I.
- Time all: repeat first [ reflexivity
- | progress intros
- | progress eliminate_hprop_eq
- | progress cbn [type.subst_default base.subst_default] in *
- | progress Compilers.type.inversion_type ].
+ intros v H evm pf; subst t'; cbn [eq_rect].
+ pose proof (@eq_indep_types_of_eq_types _ _ (@of_typed_ident _ idc) pidc evm evm type.eq_subst_default_relax) as H'.
+ revert v H.
+ set (idc' := idc) at 1; rewrite <- (@to_typed_of_typed_ident _ idc evm); subst idc'.
+ rewrite fold_unify.
+ cbv [folded_unify arg_types Raw.ident.assemble_ident];
+ cbn [Primitive.projT1 Primitive.projT2].
+ intros v.
+ Time do_rew_proj2_sig.
+ Time
+ repeat first [ progress cbn [eq_rect eq_sym] in *
+ | progress cbn [Primitive.projT1 Primitive.projT2 fst snd] in *
+ | clear_useless_step
+ | rewrite_sig_step
+ | specialize_sig_step
+ | generalize_proj1_sig_step
+ | progress cbv [to_typed Raw.ident.assemble_ident] in *
+ | match goal with
+ | [ |- context[@arg_types_of_typed_ident _ ?idc] ]
+ => is_var idc;
+ generalize dependent (@arg_types_of_typed_ident _ idc);
+ generalize dependent (@of_typed_ident _ idc);
+ clear idc;
+ intros
+ end
+ | progress cbv [arg_types prearg_types] in * ].
+ repeat first [ progress cbn [Primitive.projT1 Primitive.projT2 fst snd] in *
+ | match goal with
+ | [ |- context[(rew [fun x : ?T => @?A x -> @?B x] ?pf in ?f) ?y] ]
+ => rewrite (@push_rew_fun_dep T A B _ _ pf f y)
+ | [ |- context[rew [fun _ : ?T => ?P] ?pf in ?f] ]
+ => rewrite (@Equality.transport_const T P _ _ pf f)
+ | [ |- context[(rew [?P] ?pf in ?x) = ?y] ]
+ => rewrite <- (@eq_rew_moveR _ P _ _ pf x y)
+ | [ |- context[rew [fun x : ?T => option (@?P x)] ?pf in Some ?v] ]
+ => rewrite <- (@commute_eq_rect _ P (fun x => option (P x)) (fun _ => Some) _ _ pf v)
+ | [ |- iffT (Raw.ident.try_unify_split_args _ (*_ _*) = Some _) _ ]
+ => eapply iffT_trans; [ apply Raw.ident.try_unify_split_args_Some_correct | ]
+ | [ H : Raw.ident.try_unify_split_args _ (*_ _*) = Some _ |- _ ]
+ => apply Raw.ident.try_unify_split_args_Some_correct in H
+ | [ |- context[to_type_split_types_subst_default_eq ?t ?i ?evm] ]
+ => generalize (to_type_split_types_subst_default_eq t i evm); intro
+ end
+ | progress cbv [eq_rect_r] in *
+ | progress cbv [split_types_subst_default] in *
+ | progress cbn [eq_rect] in *
+ | progress destruct_head'_prod
+ | progress subst
+ | match goal with
+ | [ |- context[existT _ (Primitive.projT1 (split_types ?x)) _ = _] ]
+ => destruct (split_types x); clear x
+ | [ H : context[existT _ (Primitive.projT1 (split_types ?x)) _ = _] |- _ ]
+ => destruct (split_types x); clear x
+ | [ |- context[@eq_trans (type.type ?base_type) ?x ?y ?z ?pf1 ?pf2] ]
+ => generalize (@eq_trans (type.type base_type) x y z pf1 pf2); intro
+ end
+ | rewrite <- !eq_trans_rew_distr ].
+ Time
+ all:
+ repeat first [ apply pair
+ | progress cbn [eq_rect eq_rect_r eq_sym Sigma.path_sigT Sigma.path_sigT_uncurried f_equal] in *
+ | progress intros
+ | progress destruct_head'_sig
+ | progress destruct_head'_ex
+ | progress destruct_head'_and
+ | progress Sigma.inversion_sigma
+ | progress subst
+ | match goal with
+ | [ H : forall pf : ?x = ?x, _ |- _ ] => specialize (H eq_refl)
+ | [ H : lift_type_of_list_map _ ?f = _ |- _ ]
+ => is_var f; symmetry in H; destruct H; clear f
+ | [ H : context[@eq_trans (type.type ?base_type) ?x ?y ?z ?pf1 ?pf2] |- _ ]
+ => generalize dependent (@eq_trans (type.type base_type) x y z pf1 pf2); intros
+ | [ H : context[type.subst_default (type.relax _) _] |- _ ]
+ => rewrite type.eq_subst_default_relax in H
+ | [ H : ?x = ?x |- _ ] => clear H
+ | [ H : type.subst_default ?t ?evm = type.subst_default ?t ?evm'
+ |- context[lift_type_of_list_map (@subst_default_kind_of_type ?evm) (snd (Primitive.projT2 (split_types ?idc)))] ]
+ => let H' := fresh in
+ pose proof (@eq_indep_types_of_eq_types t idc idc evm evm' H eq_refl) as H';
+ cbv [split_types_subst_default] in H';
+ cbn [eq_rect_r eq_rect eq_sym Primitive.projT2 Primitive.projT1 fst snd] in H';
+ rewrite H' in *; clear H';
+ generalize dependent (type.subst_default t evm); intros; subst; clear evm
+ end
+ | rewrite <- !eq_trans_rew_distr in *
+ | eexists; rewrite <- !eq_trans_rew_distr, concat_pV
+ | match goal with
+ | [ H : _ = type.subst_default ?t ?evm |- _ ]
+ => is_var t; is_var evm;
+ generalize dependent (type.subst_default t evm); intros
+ end
+ | progress eliminate_hprop_eq ].
Qed.
Lemma unify_of_typed_ident {t idc}
: unify (@of_typed_ident t idc) idc <> None.
Proof.
- destruct idc; cbn; break_innermost_match; exact Some_neq_None.
+ rewrite fold_unify.
+ cbv [folded_unify].
+ Time do_rew_proj2_sig.
+ generalize (of_typed_ident idc), (arg_types_of_typed_ident idc); intros.
+ repeat first [ progress rewrite ?push_rew_fun_dep, ?transport_const
+ | progress cbv [eq_rect_r] in *
+ | intro
+ | match goal with
+ | [ H : (rew [?P] ?pf in ?v) = ?v2 |- _ ] => apply (@rew_r_moveL _ P _ _ pf v v2) in H
+ | [ H : context[rew [fun x : ?T => option (@?P x)] ?pf in @None ?K] |- _ ]
+ => let H' := fresh in
+ pose proof (@commute_eq_rect _ (fun _ => True) (fun x => option (P x)) (fun _ _ => @None _) _ _ pf I) as H';
+ setoid_rewrite <- H' in H;
+ clear H'
+ | [ H : @Raw.ident.try_unify_split_args ?a ?b ?c ?d ?e = None |- _ ]
+ => let H' := fresh in
+ pose proof (@Raw.ident.try_unify_split_args_None_correct a b c d e H) as H';
+ clear H
+ | [ H : forall pf : _ = _, _ |- _ ] => specialize (H eq_refl)
+ end
+ | assumption ].
Qed.
End ident.
End pattern.
diff --git a/src/Rewriter.v b/src/Rewriter.v
index e1b537959..c619d5770 100644
--- a/src/Rewriter.v
+++ b/src/Rewriter.v
@@ -2138,7 +2138,7 @@ Module Compilers.
pattern.Ident (pattern.ident.of_typed_ident (@ident.Literal t DefaultValue.type.base.default)).
Let pident_pair
- := ltac:(let v := (eval cbv [pattern.ident.of_typed_ident] in
+ := ltac:(let v := (eval cbv in
(fun A B => pattern.ident.of_typed_ident (@ident.pair A B))) in
let h := lazymatch v with fun A B => ?f _ _ => f end in
exact h).
@@ -2456,7 +2456,7 @@ Module Compilers.
:= @Compile.Rewrite (rewrite_head data) (default_fuel data) t e.
Ltac Reify include_interp specs :=
- let lems := Reify.Reify_list ident ident.reify pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_of_list_arg_types_beq) (@pattern.ident.of_typed_ident) (@pattern.ident.arg_types_of_typed_ident) (@Compile.reflect_ident_iota) (fun var t => @SubstVarLike.is_var_fst_snd_pair_opp_cast var (type.base t)) specs in
+ let lems := Reify.Reify_list ident ident.reify pattern.ident (@pattern.ident.arg_types_unfolded) (@pattern.ident.type_of_list_arg_types_beq_unfolded) (@pattern.ident.of_typed_ident_unfolded) (@pattern.ident.arg_types_of_typed_ident_unfolded) (@Compile.reflect_ident_iota) (fun var t => @SubstVarLike.is_var_fst_snd_pair_opp_cast var (type.base t)) specs in
lazymatch include_interp with
| true
=> let myapp := (eval cbv [List.app] in (@List.app)) in
diff --git a/src/RewriterWf1.v b/src/RewriterWf1.v
index 2788d7444..17ec0638d 100644
--- a/src/RewriterWf1.v
+++ b/src/RewriterWf1.v
@@ -3297,7 +3297,9 @@ Module Compilers.
let h' := lazymatch type of H with
| context[Compile.rewrite_rules_goodT_curried_cps ?pident_arg_types ?rew1] => head rew1
end in
- cbv [h' pident_arg_types Compile.rewrite_rules_goodT_curried_cps] in H;
+ let pident_arg_types' := (eval cbv -[base.interp] in pident_arg_types) in
+ change pident_arg_types with pident_arg_types' in H;
+ cbv [h' Compile.rewrite_rules_goodT_curried_cps] in H;
(* make [Qed] not take forever by explicitly recording a cast node *)
let H' := fresh in
pose proof H as H'; clear H;
@@ -3424,7 +3426,12 @@ Module Compilers.
cbv [Make.GoalType.rewrite_rules dummy_count rewrite_rules_specs] in * |- ;
let h' := lazymatch type of H with context[Compile.rewrite_rules_interp_goodT_curried_cps _ _ _ ?v] => head v end in
unfold h' in H at 1;
- cbv [Compile.rewrite_rules_interp_goodT_curried_cps pident_arg_types pident_to_typed] in H;
+ let pident_arg_types' := (eval cbv -[base.interp] in pident_arg_types) in
+ change pident_arg_types with pident_arg_types' in H;
+ let pident_to_typed' := (eval cbv -[pattern.type.subst_default pattern.base.subst_default List.fold_right base.interp base.base_interp Datatypes.fst Datatypes.snd] in pident_to_typed) in
+ let pident_to_typed' := (eval cbn [Datatypes.fst Datatypes.snd List.fold_right] in pident_to_typed') in
+ change pident_to_typed with pident_to_typed' in H;
+ cbv [Compile.rewrite_rules_interp_goodT_curried_cps] in H;
cbn [snd hd tl projT1 projT2] in H;
(* make [Qed] not take forever by explicitly recording a cast node *)
let H' := fresh in
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-18 16:33:41 +0000