aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2019-04-09 21:27:59 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2019-04-12 20:53:24 -0400
commit1384a29170bbb8b166b90f73bafea8d1948568af (patch)
tree71155a0b5501cd136c888255cb26164438521507
parentf626f41c8c5df7eb4131d16f8cc6e05140fd509c (diff)
Replace the python script with Ltac code
We now rely on Ltac rather than python to generate the raw identifiers. After | File Name | Before || Change | % Change ----------------------------------------------------------------------------------------------- 22m05.90s | Total | 21m51.87s || +0m14.03s | +1.07% ----------------------------------------------------------------------------------------------- 0m49.25s | GENERATEDIdentifiersWithoutTypesProofs.vo | 0m55.23s || -0m05.97s | -10.82% 0m19.14s | GENERATEDIdentifiersWithoutTypes.vo | 0m13.35s || +0m05.79s | +43.37% 0m36.52s | ExtractionHaskell/saturated_solinas | 0m32.60s || +0m03.92s | +12.02% 0m24.00s | SlowPrimeSynthesisExamples.vo | 0m27.22s || -0m03.21s | -11.82% 0m08.55s | ExtractionOCaml/saturated_solinas.ml | 0m05.49s || +0m03.06s | +55.73% 3m24.98s | p384_32.c | 3m22.52s || +0m02.45s | +1.21% 1m03.78s | ExtractionHaskell/word_by_word_montgomery | 1m01.13s || +0m02.64s | +4.33% 0m47.85s | p521_32.c | 0m45.77s || +0m02.07s | +4.54% 1m42.64s | Fancy/Barrett256.vo | 1m41.49s || +0m01.14s | +1.13% 0m40.30s | p521_64.c | 0m42.20s || -0m01.90s | -4.50% 0m18.02s | p256_32.c | 0m19.03s || -0m01.01s | -5.30% 0m14.70s | ExtractionOCaml/unsaturated_solinas | 0m13.33s || +0m01.36s | +10.27% 0m14.28s | p434_64.c | 0m15.39s || -0m01.11s | -7.21% 0m09.82s | p224_32.c | 0m08.77s || +0m01.05s | +11.97% 0m08.59s | p384_64.c | 0m07.36s || +0m01.22s | +16.71% 0m05.18s | ExtractionHaskell/saturated_solinas.hs | 0m06.59s || -0m01.41s | -21.39% 1m34.02s | RewriterWf2.vo | 1m34.23s || -0m00.20s | -0.22% 0m56.16s | Rewriter/ToFancyWithCasts.vo | 0m55.41s || +0m00.75s | +1.35% 0m45.85s | Rewriter/NBE.vo | 0m45.23s || +0m00.62s | +1.37% 0m44.51s | Rewriter/ArithWithCasts.vo | 0m44.12s || +0m00.39s | +0.88% 0m44.10s | RewriterInterpProofs1.vo | 0m43.89s || +0m00.21s | +0.47% 0m43.66s | ExtractionHaskell/unsaturated_solinas | 0m43.25s || +0m00.40s | +0.94% 0m36.46s | PushButtonSynthesis/UnsaturatedSolinas.vo | 0m36.36s || +0m00.10s | +0.27% 0m36.09s | RewriterWf1.vo | 0m36.07s || +0m00.02s | +0.05% 0m34.50s | Fancy/Montgomery256.vo | 0m34.30s || +0m00.20s | +0.58% 0m27.13s | PushButtonSynthesis/WordByWordMontgomery.vo | 0m26.99s || +0m00.14s | +0.51% 0m24.70s | Rewriter/Arith.vo | 0m24.26s || +0m00.43s | +1.81% 0m22.75s | ExtractionOCaml/word_by_word_montgomery | 0m22.15s || +0m00.60s | +2.70% 0m20.96s | PushButtonSynthesis/BarrettReduction.vo | 0m20.74s || +0m00.22s | +1.06% 0m18.96s | p448_solinas_64.c | 0m19.32s || -0m00.35s | -1.86% 0m18.16s | secp256k1_32.c | 0m18.13s || +0m00.03s | +0.16% 0m14.62s | ExtractionOCaml/word_by_word_montgomery.ml | 0m13.77s || +0m00.84s | +6.17% 0m11.84s | ExtractionOCaml/saturated_solinas | 0m11.30s || +0m00.53s | +4.77% 0m09.55s | ExtractionOCaml/unsaturated_solinas.ml | 0m09.14s || +0m00.41s | +4.48% 0m08.42s | ExtractionHaskell/word_by_word_montgomery.hs | 0m08.16s || +0m00.25s | +3.18% 0m06.96s | BoundsPipeline.vo | 0m06.85s || +0m00.11s | +1.60% 0m06.54s | ExtractionHaskell/unsaturated_solinas.hs | 0m07.17s || -0m00.62s | -8.78% 0m03.57s | PushButtonSynthesis/Primitives.vo | 0m03.46s || +0m00.10s | +3.17% 0m03.35s | PushButtonSynthesis/SmallExamples.vo | 0m03.34s || +0m00.01s | +0.29% 0m03.30s | PushButtonSynthesis/SaturatedSolinas.vo | 0m03.22s || +0m00.07s | +2.48% 0m02.83s | curve25519_32.c | 0m02.86s || -0m00.02s | -1.04% 0m02.70s | PushButtonSynthesis/FancyMontgomeryReduction.vo | 0m02.63s || +0m00.07s | +2.66% 0m02.08s | Rewriter.vo | 0m02.02s || +0m00.06s | +2.97% 0m01.60s | curve25519_64.c | 0m01.82s || -0m00.21s | -12.08% 0m01.47s | secp256k1_64.c | 0m01.94s || -0m00.47s | -24.22% 0m01.34s | p224_64.c | 0m01.71s || -0m00.36s | -21.63% 0m01.33s | CLI.vo | 0m01.38s || -0m00.04s | -3.62% 0m01.32s | p256_64.c | 0m01.77s || -0m00.44s | -25.42% 0m01.28s | Rewriter/ToFancy.vo | 0m01.36s || -0m00.08s | -5.88% 0m01.23s | Rewriter/StripLiteralCasts.vo | 0m01.08s || +0m00.14s | +13.88% 0m01.16s | StandaloneHaskellMain.vo | 0m01.18s || -0m00.02s | -1.69% 0m01.13s | CompilersTestCases.vo | 0m01.18s || -0m00.05s | -4.23% 0m01.07s | StandaloneOCamlMain.vo | 0m01.12s || -0m00.05s | -4.46% 0m00.83s | RewriterAll.vo | 0m00.66s || +0m00.16s | +25.75% 0m00.78s | RewriterAllTactics.vo | 0m00.83s || -0m00.04s | -6.02%
-rw-r--r--src/GENERATEDIdentifiersWithoutTypes.v3769
-rw-r--r--src/GENERATEDIdentifiersWithoutTypesProofs.v89
-rw-r--r--src/Rewriter.v25
3 files changed, 968 insertions, 2915 deletions
diff --git a/src/GENERATEDIdentifiersWithoutTypes.v b/src/GENERATEDIdentifiersWithoutTypes.v
index 3dfa4713b..1fca4e115 100644
--- a/src/GENERATEDIdentifiersWithoutTypes.v
+++ b/src/GENERATEDIdentifiersWithoutTypes.v
@@ -1,4 +1,5 @@
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.
@@ -10,1040 +11,65 @@ Require Import Crypto.Util.PrimitiveSigma.
Require Import Crypto.Util.Bool.Reflect.
Require Import Crypto.Util.Notations.
Require Import Crypto.Language.
+Require Import Crypto.Util.Tactics.Head.
+Require Import Crypto.Util.Tactics.ConstrFail.
+Require Import Crypto.Util.Tactics.CacheTerm.
+Require Crypto.Util.Tuple.
Import ListNotations. Local Open Scope list_scope.
Import PrimitiveSigma.Primitive.
Module Compilers.
Set Boolean Equality Schemes.
Set Decidable Equality Schemes.
+ Local Set Primitive Projections.
Export Language.Compilers.
+ Local Notation "'plet' x := y 'in' z" := (match y return _ with x => z end).
Local Notation type_of_list := (fold_right (fun A B => prod A B) unit).
Local Notation type_of_list_cps := (fold_right (fun a K => a -> K)).
- Module pattern.
- Notation EvarMap := (PositiveMap.t Compilers.base.type).
- Module base.
- Local Notation einterp := type.interp.
- Module type.
- Inductive type := var (p : positive) | type_base (t : Compilers.base.type.base) | prod (A B : type) | list (A : type) | option (A : type).
- End type.
- Notation type := type.type.
-
- Fixpoint relax (t : Compilers.base.type) : type
- := match t with
- | Compilers.base.type.type_base t => type.type_base t
- | Compilers.base.type.prod A B => type.prod (relax A) (relax B)
- | Compilers.base.type.list A => type.list (relax A)
- | Compilers.base.type.option A => type.option (relax A)
- end.
-
- Definition lookup_default (p : positive) (evar_map : EvarMap) : Compilers.base.type
- := match PositiveMap.find p evar_map with
- | Datatypes.Some t => t
- | Datatypes.None => Compilers.base.type.type_base base.type.unit
- end.
-
- Fixpoint subst_default (ptype : type) (evar_map : EvarMap) : Compilers.base.type
- := match ptype with
- | type.var p => lookup_default p evar_map
- | type.type_base t => Compilers.base.type.type_base t
- | type.prod A B
- => Compilers.base.type.prod (subst_default A evar_map) (subst_default B evar_map)
- | type.list A => Compilers.base.type.list (subst_default A evar_map)
- | type.option A => Compilers.base.type.option (subst_default A evar_map)
- end.
-
- Fixpoint collect_vars (t : type) : PositiveSet.t
- := match t with
- | type.var p => PositiveSet.add p PositiveSet.empty
- | type.type_base t => PositiveSet.empty
- | type.prod A B => PositiveSet.union (collect_vars A) (collect_vars B)
- | type.list A => collect_vars A
- | type.option A => collect_vars A
- end.
-
- Module Notations.
- Global Coercion type.type_base : Compilers.base.type.base >-> type.type.
- Bind Scope pbtype_scope with type.type.
- (*Bind Scope ptype_scope with Compilers.type.type type.type.*) (* COQBUG(https://github.com/coq/coq/issues/7699) *)
- Delimit Scope ptype_scope with ptype.
- Delimit Scope pbtype_scope with pbtype.
- Notation "A * B" := (type.prod A%ptype B%ptype) : ptype_scope.
- Notation "A * B" := (type.prod A%pbtype B%pbtype) : pbtype_scope.
- Notation "()" := (type.type_base base.type.unit) : pbtype_scope.
- Notation "()" := (type.base (type.type_base base.type.unit)) : ptype_scope.
- Notation "A -> B" := (type.arrow A%ptype B%ptype) : ptype_scope.
- Notation "' n" := (type.var n) : pbtype_scope.
- Notation "' n" := (type.base (type.var n)) : ptype_scope.
- Notation "'1" := (type.var 1) : pbtype_scope.
- Notation "'2" := (type.var 2) : pbtype_scope.
- Notation "'3" := (type.var 3) : pbtype_scope.
- Notation "'4" := (type.var 4) : pbtype_scope.
- Notation "'5" := (type.var 5) : pbtype_scope.
- Notation "'1" := (type.base (type.var 1)) : ptype_scope.
- Notation "'2" := (type.base (type.var 2)) : ptype_scope.
- Notation "'3" := (type.base (type.var 3)) : ptype_scope.
- Notation "'4" := (type.base (type.var 4)) : ptype_scope.
- Notation "'5" := (type.base (type.var 5)) : ptype_scope.
- End Notations.
- End base.
- Notation type := (type.type base.type).
- Export base.Notations.
- Module type.
- Fixpoint relax (t : type.type Compilers.base.type) : type
- := match t with
- | type.base t => type.base (base.relax t)
- | type.arrow s d => type.arrow (relax s) (relax d)
- end.
-
- Fixpoint subst_default (ptype : type) (evar_map : EvarMap) : type.type Compilers.base.type
- := match ptype with
- | type.base t => type.base (base.subst_default t evar_map)
- | type.arrow A B => type.arrow (subst_default A evar_map) (subst_default B evar_map)
- end.
+ Definition app_type_of_list {K} {ls : list Type} (f : type_of_list_cps K ls) (args : type_of_list ls) : K
+ := list_rect
+ (fun ls
+ => type_of_list_cps K ls -> type_of_list ls -> K)
+ (fun v _ => v)
+ (fun T Ts rec f x
+ => rec (f (fst x)) (snd x))
+ ls
+ f args.
+
+ Definition lam_type_of_list {ls K} : (type_of_list ls -> K) -> type_of_list_cps K ls
+ := list_rect
+ (fun ls => (type_of_list ls -> K) -> type_of_list_cps K ls)
+ (fun f => f tt)
+ (fun T Ts rec k t => rec (fun ts => k (t, ts)))
+ ls.
+
+ Fixpoint list_app_type_of_list {ls1 ls2 : list Type} : type_of_list ls1 -> type_of_list ls2 -> type_of_list (ls1 ++ ls2)
+ := match ls1 return type_of_list ls1 -> type_of_list ls2 -> type_of_list (ls1 ++ ls2) with
+ | nil => fun _ x => x
+ | cons T Ts => fun tts rest => (fst tts, @list_app_type_of_list Ts ls2 (snd tts) rest)
+ end.
+
+ Fixpoint list_unapp_type_of_list {ls1 ls2 : list Type} : type_of_list (ls1 ++ ls2) -> type_of_list ls1 * type_of_list ls2
+ := match ls1 return type_of_list (ls1 ++ ls2) -> type_of_list ls1 * type_of_list ls2 with
+ | nil => fun x => (tt, x)
+ | cons T Ts
+ => fun tts
+ => let '(t2, t2s) := @list_unapp_type_of_list Ts ls2 (snd tts) in
+ (fst tts, t2, t2s)
+ end.
+
+ Fixpoint lift_type_of_list_map {A} {ls : list A} {P1 P2 : A -> Type} (F : forall a, P1 a -> P2 a) {struct ls}
+ : type_of_list (List.map P1 ls) -> type_of_list (List.map P2 ls)
+ := match ls return type_of_list (List.map P1 ls) -> type_of_list (List.map P2 ls) with
+ | 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))
+ end.
- Fixpoint collect_vars (t : type) : PositiveSet.t
- := match t with
- | type.base t => base.collect_vars t
- | type.arrow s d => PositiveSet.union (collect_vars s) (collect_vars d)
- end.
- End type.
-
- (*
- Set Printing Coercions.
- Redirect "/tmp/pr" Print Compilers.ident.ident.
- Redirect "/tmp/sm" Show Match Compilers.ident.ident.
- *)
- (*
-<<<
-#!/usr/bin/env python2
-import re, os
-
-print_ident = r"""Inductive ident : defaults.type -> Set :=
- Literal : forall t : base.type.base,
- base.interp (Compilers.base.type.type_base t) ->
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base t))
- | Nat_succ : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat))%ptype
- | Nat_pred : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat))%ptype
- | Nat_max : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat))%ptype
- | Nat_mul : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat))%ptype
- | Nat_add : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat))%ptype
- | Nat_sub : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat))%ptype
- | Nat_eqb : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.bool))%ptype
- | nil : forall t : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list t))
- | cons : forall t : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x) t ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list t) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list t))%ptype
- | pair : forall A B : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x) A ->
- (fun x : Compilers.base.type => type.base x) B ->
- (fun x : Compilers.base.type => type.base x) (A * B)%etype)%ptype
- | fst : forall A B : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x) (A * B)%etype ->
- (fun x : Compilers.base.type => type.base x) A)%ptype
- | snd : forall A B : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x) (A * B)%etype ->
- (fun x : Compilers.base.type => type.base x) B)%ptype
- | prod_rect : forall A B T : Compilers.base.type,
- ident
- (((fun x : Compilers.base.type => type.base x) A ->
- (fun x : Compilers.base.type => type.base x) B ->
- (fun x : Compilers.base.type => type.base x) T) ->
- (fun x : Compilers.base.type => type.base x) (A * B)%etype ->
- (fun x : Compilers.base.type => type.base x) T)%ptype
- | bool_rect : forall T : Compilers.base.type,
- ident
- (((fun x : Compilers.base.type => type.base x) ()%etype ->
- (fun x : Compilers.base.type => type.base x) T) ->
- ((fun x : Compilers.base.type => type.base x) ()%etype ->
- (fun x : Compilers.base.type => type.base x) T) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.bool) ->
- (fun x : Compilers.base.type => type.base x) T)%ptype
- | nat_rect : forall P : Compilers.base.type,
- ident
- (((fun x : Compilers.base.type => type.base x) ()%etype ->
- (fun x : Compilers.base.type => type.base x) P) ->
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x) P ->
- (fun x : Compilers.base.type => type.base x) P) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x) P)%ptype
- | nat_rect_arrow : forall 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)
- (Compilers.base.type.type_base base.type.nat) ->
- ((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.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x) P ->
- (fun x : Compilers.base.type => type.base x) Q)%ptype
- | eager_nat_rect : forall P : Compilers.base.type,
- ident
- (((fun x : Compilers.base.type => type.base x)
- ()%etype ->
- (fun x : Compilers.base.type => type.base x) P) ->
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x) P ->
- (fun x : Compilers.base.type => type.base x) P) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x) P)%ptype
- | eager_nat_rect_arrow : forall 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)
- (Compilers.base.type.type_base base.type.nat) ->
- ((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.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x) P ->
- (fun x : Compilers.base.type => type.base x) Q)%ptype
- | list_rect : forall A P : Compilers.base.type,
- ident
- (((fun x : Compilers.base.type => type.base x) ()%etype ->
- (fun x : Compilers.base.type => type.base x) P) ->
- ((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) P) ->
- (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)
- ()%etype ->
- (fun x : Compilers.base.type => type.base x) P) ->
- ((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) P) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A) ->
- (fun x : Compilers.base.type => type.base x) P)%ptype
- | eager_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
- | list_case : forall A P : Compilers.base.type,
- ident
- (((fun x : Compilers.base.type => type.base x) ()%etype ->
- (fun x : Compilers.base.type => type.base x) P) ->
- ((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)
- (Compilers.base.type.list A) ->
- (fun x : Compilers.base.type => type.base x) P)%ptype
- | List_length : forall T : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list T) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat))%ptype
- | List_seq : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list
- (Compilers.base.type.type_base base.type.nat)))%ptype
- | List_firstn : forall A : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A))%ptype
- | List_skipn : forall A : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A))%ptype
- | List_repeat : forall A : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x) A ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A))%ptype
- | List_combine : forall A B : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list B) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list (A * B)))%ptype
- | List_map : forall A B : Compilers.base.type,
- ident
- (((fun x : Compilers.base.type => type.base x) A ->
- (fun x : Compilers.base.type => type.base x) B) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list B))%ptype
- | List_app : forall A : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A))%ptype
- | List_rev : forall A : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A))%ptype
- | List_flat_map : forall A B : Compilers.base.type,
- ident
- (((fun x : Compilers.base.type => type.base x) A ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list B)) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list B))%ptype
- | List_partition : forall A : Compilers.base.type,
- ident
- (((fun x : Compilers.base.type => type.base x) A ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.bool)) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list A *
- Compilers.base.type.list A)%etype)%ptype
- | List_fold_right : forall A B : Compilers.base.type,
- ident
- (((fun x : Compilers.base.type => type.base x) B ->
- (fun x : Compilers.base.type => type.base x) A ->
- (fun x : Compilers.base.type => type.base x) A) ->
- (fun x : Compilers.base.type => type.base x) A ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list B) ->
- (fun x : Compilers.base.type => type.base x) A)%ptype
- | List_update_nth : forall T : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- ((fun x : Compilers.base.type => type.base x) T ->
- (fun x : Compilers.base.type => type.base x) T) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list T) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list T))%ptype
- | List_nth_default : forall T : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x) T ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list T) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x) T)%ptype
- | eager_List_nth_default : forall T : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x)
- T ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.list T) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base
- base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- T)%ptype
- | Z_add : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_mul : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_pow : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_sub : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_opp : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_div : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_modulo : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_log2 : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_log2_up : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_eqb : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.bool))%ptype
- | Z_leb : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.bool))%ptype
- | Z_ltb : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.bool))%ptype
- | Z_geb : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.bool))%ptype
- | Z_gtb : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.bool))%ptype
- | Z_of_nat : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_to_nat : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.nat))%ptype
- | Z_shiftr : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_shiftl : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_land : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_lor : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_min : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_max : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_bneg : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_lnot_modulo : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_mul_split : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | Z_add_get_carry : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | Z_add_with_carry : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_add_with_get_carry : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | Z_sub_get_borrow : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | Z_sub_with_get_borrow : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | Z_zselect : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_add_modulo : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_rshi : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_cc_m : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_combine_at_bitwidth : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_cast : zrange ->
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_cast2 : zrange * zrange ->
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | option_Some : forall A : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x) A ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.option A))%ptype
- | option_None : forall A : Compilers.base.type,
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.option A))
- | option_rect : forall A P : Compilers.base.type,
- ident
- (((fun x : Compilers.base.type => type.base x) A ->
- (fun x : Compilers.base.type => type.base x) P) ->
- ((fun x : Compilers.base.type => type.base x) ()%etype ->
- (fun x : Compilers.base.type => type.base x) P) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.option A) ->
- (fun x : Compilers.base.type => type.base x) P)%ptype
- | Build_zrange : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.zrange))%ptype
- | zrange_rect : forall P : Compilers.base.type,
- ident
- (((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z) ->
- (fun x : Compilers.base.type => type.base x) P) ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.zrange) ->
- (fun x : Compilers.base.type => type.base x) P)%ptype
- | fancy_add : Z ->
- Z ->
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | fancy_addc : Z ->
- Z ->
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | fancy_sub : Z ->
- Z ->
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | fancy_subb : Z ->
- Z ->
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | fancy_mulll : Z ->
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_mullh : Z ->
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_mulhl : Z ->
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_mulhh : Z ->
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_rshi : Z ->
- Z ->
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_selc : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_selm : Z ->
- ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_sell : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_addm : ident
- ((fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z *
- Compilers.base.type.type_base base.type.Z)%etype ->
- (fun x : Compilers.base.type => type.base x)
- (Compilers.base.type.type_base base.type.Z))%ptype
-
-"""
-show_match_ident = r"""match # with
- | ident.Literal t v =>
- | ident.Nat_succ =>
- | ident.Nat_pred =>
- | ident.Nat_max =>
- | ident.Nat_mul =>
- | ident.Nat_add =>
- | ident.Nat_sub =>
- | ident.Nat_eqb =>
- | ident.nil t =>
- | ident.cons t =>
- | ident.pair A B =>
- | ident.fst A B =>
- | ident.snd A B =>
- | ident.prod_rect A B T =>
- | ident.bool_rect T =>
- | ident.nat_rect P =>
- | ident.nat_rect_arrow P Q =>
- | 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 =>
- | ident.List_length T =>
- | ident.List_seq =>
- | ident.List_firstn A =>
- | ident.List_skipn A =>
- | ident.List_repeat A =>
- | ident.List_combine A B =>
- | ident.List_map A B =>
- | ident.List_app A =>
- | ident.List_rev A =>
- | ident.List_flat_map A B =>
- | ident.List_partition A =>
- | ident.List_fold_right A B =>
- | ident.List_update_nth T =>
- | ident.List_nth_default T =>
- | ident.eager_List_nth_default T =>
- | ident.Z_add =>
- | ident.Z_mul =>
- | ident.Z_pow =>
- | ident.Z_sub =>
- | ident.Z_opp =>
- | ident.Z_div =>
- | ident.Z_modulo =>
- | ident.Z_log2 =>
- | ident.Z_log2_up =>
- | ident.Z_eqb =>
- | ident.Z_leb =>
- | ident.Z_ltb =>
- | ident.Z_geb =>
- | ident.Z_gtb =>
- | ident.Z_of_nat =>
- | ident.Z_to_nat =>
- | ident.Z_shiftr =>
- | ident.Z_shiftl =>
- | ident.Z_land =>
- | ident.Z_lor =>
- | ident.Z_min =>
- | ident.Z_max =>
- | ident.Z_bneg =>
- | ident.Z_lnot_modulo =>
- | ident.Z_mul_split =>
- | ident.Z_add_get_carry =>
- | ident.Z_add_with_carry =>
- | ident.Z_add_with_get_carry =>
- | ident.Z_sub_get_borrow =>
- | ident.Z_sub_with_get_borrow =>
- | ident.Z_zselect =>
- | ident.Z_add_modulo =>
- | ident.Z_rshi =>
- | ident.Z_cc_m =>
- | ident.Z_combine_at_bitwidth =>
- | ident.Z_cast range =>
- | ident.Z_cast2 range =>
- | ident.option_Some A =>
- | ident.option_None A =>
- | ident.option_rect A P =>
- | ident.Build_zrange =>
- | ident.zrange_rect P =>
- | ident.fancy_add log2wordmax imm =>
- | ident.fancy_addc log2wordmax imm =>
- | ident.fancy_sub log2wordmax imm =>
- | ident.fancy_subb log2wordmax imm =>
- | ident.fancy_mulll log2wordmax =>
- | ident.fancy_mullh log2wordmax =>
- | ident.fancy_mulhl log2wordmax =>
- | ident.fancy_mulhh log2wordmax =>
- | ident.fancy_rshi log2wordmax x =>
- | ident.fancy_selc =>
- | ident.fancy_selm log2wordmax =>
- | ident.fancy_sell =>
- | ident.fancy_addm =>
- end
-
-"""
-remake = False
-if remake:
- assert(os.path.exists('/tmp/pr.out'))
- assert(os.path.exists('/tmp/sm.out'))
- with open('/tmp/pr.out', 'r') as f: print_ident = re.sub(r'^For [^ ]*: Argument.*', '', f.read(), flags=re.MULTILINE|re.DOTALL)
- with open('/tmp/sm.out', 'r') as f: show_match_ident = f.read()
-
-prefix = 'Compilers.'
-indent0 = ' '
-indent1 = ' ' + indent0
-indent2 = ' ' + indent1
-#exts = ('Unit', 'Z', 'Bool', 'Nat')
-base_types = [('%sbase.type.' % prefix) + i for i in ('unit', 'Z', 'bool', 'nat', 'zrange')]
-type_or_set = 'Type'
-ctors = [i.strip('|=> ').split(' ') for i in show_match_ident.split('\n') if i.strip().startswith('|')]
-assert(ctors[0][0] == 'ident.Literal')
-assert(len(ctors[0]) > 1)
-#ctors = [[ctors[0][0] + ext] + ctors[0][2:] for ext in exts] + ctors[1:]
-ctors_with_prefix = [[prefix + i[0]] + i[1:] for i in ctors]
-ctors_no_prefix = [[i[0].replace('ident.', '')] + i[1:] for i in ctors]
-pctors = [i[0] for i in ctors_no_prefix]
-def get_dep_types(case):
- dep_tys = re.findall('forall ([^:]+):([^,]+),', case)
- if len(dep_tys) == 0: return []
- dep_tys = dep_tys[0]
- return [dep_tys[-1].strip()] * len([i for i in dep_tys[0].split(' ') if i.strip()])
-split_print_ident = print_ident.replace(' Literal ', ' | Literal ').replace('\n', ' ').split('|')[1:]
-ttypes = [get_dep_types(case) for case in split_print_ident]
-ctypes = [[i.strip() for i in re.sub(r'forall [^,]+,', '', i[i.find(':')+1:i.find('ident')]).strip(' ->').split('->') if i.strip()]
- for i in split_print_ident]
-crettypes = [prefix + 'ident.' + re.sub(r'\(fun x : [^ ]+ => ([^ ]+) x\)', r'\1', re.sub(' +', ' ', i[i.find('ident'):])).strip()
- for i in split_print_ident]
-named_ttypes_with_prefix = [[(name, ty) for name, ty in zip(ctor[1:], tys)]
- for ctor, tys in zip(ctors, ttypes)]
-named_ttypes = [[(name, ty.replace(prefix, '')) for name, ty in nt] for nt in named_ttypes_with_prefix]
-pctors_with_typed_args = [(pctor + ' ' + ' '.join('{%s : %s}' % name_ty for name_ty in ntys)).strip()
- for pctor, ntys in zip(pctors, named_ttypes)]
-pctors_with_args = [(pctor + ' ' + ' '.join(name for name, ty in ntys)).strip()
- for pctor, ntys in zip(pctors, named_ttypes)]
-pctors_with_underscores = [(pctor + ' ' + ' '.join('_' for name, ty in ntys)).strip()
- for pctor, ntys in zip(pctors, named_ttypes)]
-rettypes = [i.replace(prefix + 'ident.ident', 'ident').replace(prefix, '').replace('%etype', '%pbtype') for i in crettypes]
-
-# N.B. We assume forall-quantification in the types has names that match the arguments from Show Match
-
-retcode = r"""Require Import Coq.ZArith.ZArith.
-Require Import Coq.FSets.FMapPositive.
-Require Import Coq.MSets.MSetPositive.
-Require Import Coq.Lists.List.
-Require Import Coq.derive.Derive.
-Require Import Crypto.Util.CPSNotations.
-Require Import Crypto.Util.Option.
-Require Import Crypto.Util.ZRange.
-Require Import Crypto.Util.PrimitiveSigma.
-Require Import Crypto.Util.Bool.Reflect.
-Require Import Crypto.Util.Notations.
-Require Import Crypto.Language.
-Import ListNotations. Local Open Scope list_scope.
-Import PrimitiveSigma.Primitive.
-
-Module Compilers.
- Set Boolean Equality Schemes.
- Set Decidable Equality Schemes.
- Export Language.Compilers.
-
- Local Notation type_of_list := (fold_right (fun A B => prod A B) unit).
- Local Notation type_of_list_cps := (fold_right (fun a K => a -> K)).
Module pattern.
Notation EvarMap := (PositiveMap.t Compilers.base.type).
Module base.
@@ -1134,364 +160,133 @@ Module Compilers.
end.
End type.
- (""" + """*
- Set Printing Coercions.
- Redirect "/tmp/pr" Print Compilers.ident.ident.
- Redirect "/tmp/sm" Show Match Compilers.ident.ident.
- *""" + """)
-"""
-
-def fold_right_pair(ls, tt='tt'):
- if len(ls) == 0: return tt
- return '(' + ls[0] + ', ' + fold_right_pair(ls[1:], tt=tt) + ')'
-
-def addnewline(s): return re.sub(r' +$', '', s + '\n', flags=re.MULTILINE)
-
-def get_updated_contents():
- contents = open(__file__).read()
- contents = re.sub(r'^remake = True', r'remake = False', contents, flags=re.MULTILINE)
- contents = re.sub(r'^print_ident = r""".*?"""', r'print_ident = r"""' + print_ident + r'"""', contents, flags=re.MULTILINE | re.DOTALL)
- contents = re.sub(r'^show_match_ident = r""".*?"""', r'show_match_ident = r"""' + show_match_ident + r'"""', contents, flags=re.MULTILINE | re.DOTALL)
- return contents
-
-retcode += addnewline(r"""%s(*
-<<<
-%s
->>>
-%s*)
-""" % (indent0, get_updated_contents(), indent0))
-
-maxeta = max([len(ttype + ctype) for ttype, ctype in zip(ttypes, ctypes)])
-#if any(len(ttype) > 0 and len(ctype) > 0 for ttype, ctype in zip(ttypes, ctypes)):
-# retcode += addnewline(r"""%sLocal Notation eta_sigT x := (existT _ (projT1 x) (projT2 x)) (only parsing).""" % indent0)
-if maxeta >= 2:
- retcode += addnewline(r"""%sLocal Notation eta2 x := (Datatypes.fst x, Datatypes.snd x) (only parsing).""" % indent0)
- retcode += addnewline(r"""%sLocal Notation eta2r x := (Datatypes.fst x, Datatypes.snd x) (only parsing).""" % indent0)
-for i in range(3, maxeta+1):
- retcode += addnewline(r"""%sLocal Notation eta%d x := (eta%d (Datatypes.fst x), Datatypes.snd x) (only parsing).""" % (indent0, i, i-1))
- retcode += addnewline(r"""%sLocal Notation eta%dr x := (Datatypes.fst x, eta%dr (Datatypes.snd x)) (only parsing).""" % (indent0, i, i-1))
-retcode += addnewline('')
-
-def do_adjust_type(ctor, ctype):
- return len(ctor) > 1 and 'Literal' in ctor[0]
-
-retcode += r"""
- Module Raw.
- Module ident.
-"""
-
-retcode += addnewline(r"""%sInductive ident :=
-%s| %s.
-""" % (indent2, indent2, ('\n' + indent2 + '| ').join(pctors)))
-
-def make_prod_of_types(named_ttype, ctype):
- if len(named_ttype + ctype) == 0: return 'unit'
- if len(ctype) == 0: return ' * '.join(t for n, t in named_ttype)
- if len(named_ttype) == 0: return ' * '.join(ctype)
- if len(named_ttype) == 1: return '{ %s : %s & %s }' % (named_ttype[0][0], named_ttype[0][1], ' * '.join(ctype))
- return "{ tys : %s & let '(%s) := eta%d tys in %s }" % (' * '.join(t for n, t in named_ttype),
- ', '.join(n for n, t in named_ttype),
- len(named_ttype),
- ' * '.join(ctype))
-
-def make_pair_of_types(named_ttype, ctype, ctor):
- if len(named_ttype + ctype) == 0: return 'tt'
- if len(named_ttype + ctype) == 1: return ctor[-1]
- if len(named_ttype) == 0 or len(ctype) == 0: return '(%s)' % ', '.join(ctor[-len(named_ttype + ctype):])
- pr1 = (named_ttype[0][0] if len(named_ttype) == 1 else '(%s)' % ', '.join(n for n, t in named_ttype))
- pr2 = (ctor[-1] if len(ctype) == 1 else '(%s)' % ', '.join(ctor[-len(ctype):]))
- return '(existT _ %s %s)' % (pr1, pr2)
-
-def make_fun_project(named_ttype, ctype, ctor):
- if len(named_ttype + ctype) == 0: return 'fun _ => '
- if len(named_ttype + ctype) == 1: return 'fun ' + ctor[-1] + ' => '
- if len(named_ttype) == 0 or len(ctype) == 0: return "fun arg => let '(%s) := eta%d arg in " % (', '.join(ctor[-len(named_ttype + ctype):]), len(named_ttype + ctype))
- pr1 = (named_ttype[0][0] if len(named_ttype) == 1 else '(%s)' % ', '.join(n for n, t in named_ttype))
- pr2 = (ctor[-1] if len(ctype) == 1 else '(%s)' % ', '.join(ctor[-len(ctype):]))
- pr1_eta = ('projT1 arg' if len(named_ttype) == 1 else 'eta%d (projT1 arg)' % len(named_ttype))
- pr2_eta = ('projT2 arg' if len(ctype) == 1 else 'eta%d (projT2 arg)' % len(ctype))
- return "fun arg => let '(%s, %s) := (%s, %s) in " % (pr1, pr2, pr1_eta, pr2_eta)
-
-def make_fun_project_list(ctype, ctor):
- if len(ctype) == 0: return 'fun _ => '
- return "fun arg => let '%s := eta%dr arg in " % (fold_right_pair(ctor[-len(ctype):], tt='_'), len(ctype)+1)
-
-def make_fun_project_match(named_ttype, ctype, ctor, retty, body):
- if len(named_ttype + ctype) == 0: return 'fun _ => ' + body
- if len(named_ttype + ctype) == 1: return 'fun ' + ctor[-1] + ' => ' + body
- if len(named_ttype) == 0 or len(ctype) == 0:
- return "fun arg => match eta%d arg as arg' return %s with (%s) => %s end" % (len(named_ttype + ctype), retty % "arg'", ', '.join(ctor[-len(named_ttype + ctype):]), body)
- pr1 = (named_ttype[0][0] if len(named_ttype) == 1 else '(%s)' % ', '.join(n for n, t in named_ttype))
- pr2 = (ctor[-1] if len(ctype) == 1 else '(%s)' % ', '.join(ctor[-len(ctype):]))
- pr1_eta = ('projT1 arg' if len(named_ttype) == 1 else 'eta%d (projT1 arg)' % len(named_ttype))
- pr2_eta = ('projT2 arg' if len(ctype) == 1 else 'eta%d (projT2 arg)' % len(ctype))
- return "fun arg => match existT _ (%s) (%s) as arg' return %s with existT %s %s => %s end" % (pr1_eta, pr2_eta, retty % "arg'", pr1, pr2, body)
-
-retcode += addnewline((r"""%sDefinition full_types (idc : ident) : %s
- := match idc return %s with
- | %s
- end%%type.
-""" % (indent2, type_or_set, type_or_set,
- '\n | '.join(pctor + ' => ' + make_prod_of_types(named_ttype, ctype)
- for pctor, named_ttype, ctype in zip(pctors, named_ttypes_with_prefix, ctypes)))).replace('\n', '\n' + indent2))
-
-retcode += addnewline((r"""%sDefinition is_simple (idc : ident) : bool
- := match idc with
- | %s
- end.
-""" % (indent2,
- '\n | '.join(pctor + ' => ' + ('true' if len(named_ttype) == 0 else 'false')
- for pctor, named_ttype in zip(pctors, named_ttypes_with_prefix)))).replace('\n', '\n' + indent2))
-
-retcode += addnewline((r"""%sDefinition invert_bind_args {t} (idc : %sident.ident t) (pidc : ident) : Datatypes.option (full_types pidc)
- := match pidc, idc return Datatypes.option (full_types pidc) with
- | %s
- | %s
- => Datatypes.None
- end%%cps.
-""" % (indent2, prefix,
- '\n | '.join(pctor + ', ' + ' '.join(ctor) + ' => Datatypes.Some ' + make_pair_of_types(named_ttype, ctype, ctor)
- for pctor, ctor, named_ttype, ctype in zip(pctors, ctors_with_prefix, named_ttypes_with_prefix, ctypes)),
- '\n | '.join(pctor + ', _' for pctor in pctors))).replace('\n', '\n' + indent2))
-
-retcode += addnewline((r"""%sDefinition type_of (pidc : ident) : full_types pidc -> %stype %sbase.type
- := match pidc return full_types pidc -> _ with
- | %s
- end%%etype.
-""" % (indent2, prefix, prefix,
- '\n | '.join(pctor + ' => '
- + make_fun_project(named_ttype, ctype, ctor) + cretty.replace(prefix + 'ident.ident ', '')
- for pctor, ctor, named_ttype, ctype, cretty in zip(pctors, ctors_with_prefix, named_ttypes_with_prefix, ctypes, crettypes)))).replace('\n', '\n' + indent2))
-retcode += addnewline((r"""%sDefinition to_typed (pidc : ident) : forall args : full_types pidc, %sident.ident (type_of pidc args)
- := match pidc return forall args : full_types pidc, %sident.ident (type_of pidc args) with
- | %s
- end.
-""" % (indent2, prefix, prefix,
- '\n | '.join(pctor + ' => '
- + make_fun_project_match(named_ttype, ctype, ctor, '%sident.ident (type_of %s %%s)' % (prefix, pctor), ("@" + ' '.join(ctor)))
- for pctor, ctor, named_ttype, ctype in zip(pctors, ctors_with_prefix, named_ttypes_with_prefix, ctypes)))).replace('\n', '\n' + indent2))
-
-retcode += r""" End ident.
- Notation ident := ident.ident.
- End Raw.
-"""
-
-retcode +=r"""
- Module ident.
-"""
-retcode += addnewline((r"""%sDefinition eta_ident_cps {T : %stype %sbase.type -> Type} {t} (idc : %sident.ident t)
- (f : forall t', %sident.ident t' -> T t')
- : T t
- := match idc with
- | %s
- end.
-""" % (indent1, prefix, prefix, prefix, prefix,
- '\n | '.join(' '.join(ctor) + ' => f _ '
- + (('%s' if len(ctor) == 1 else '(@%s)')
- % ' '.join(ctor))
- for ctor in ctors_with_prefix))).replace('\n', '\n' + indent1))
-
-retcode += addnewline(r"""%sInductive ident : type -> Set :=
-%s| %s.
-""" % (indent1, indent1, ('\n' + indent1 + '| ').join('%s : %s' % ct for ct in zip(pctors_with_typed_args, rettypes))))
-
-retcode += addnewline((r"""%sDefinition strip_types {t} (idc : ident t) : Raw.ident
- := match idc with
- | %s
- end.
-""" % (indent1, '\n | '.join('@' + pctor_with_args + ' => Raw.ident.' + pctor for pctor_with_args, pctor in zip(pctors_with_args, pctors)))).replace('\n', '\n' + indent1))
-
-# here we assume that non-dependent arguments do not depend on dependent
-# arguments which become generalized to patterns --- that is, only dependent
-# arguments of type base.type.base can show up in the types of other identifier
-# arguments.
-
-retcode += addnewline((r"""%sDefinition arg_types {t} (idc : ident t) : list %s
- := match idc return list %s with
- | %s
- end%%type.
-""" % (indent1, type_or_set, type_or_set,
- '\n | '.join('@' + pctor + ' => [' + '; '.join(i + ' : ' + type_or_set for i in ctype) + ']'
- for pctor, ctype in zip(pctors_with_args, ctypes)))).replace('\n', '\n' + indent1))
-
-def to_type_var(name, ty):
- ty = ty.replace(prefix, '')
- return ({'base.type.base': 'type.base (base.type.type_base %s)' % name,
- 'base.type': 'type.base %s' % name,
- 'type': name,
- 'type.type base.type': name})[ty]
-
-#retcode += addnewline((r"""%sDefinition type_vars {t} (idc : ident t) : list type
-# := match idc with
-# | %s
-# end%%type.
-#""" % (indent1,
-# '\n | '.join('@' + pctor + ' => [' + '; '.join(to_type_var(n, t) for n, t in named_ttype) + ']'
-# for pctor, named_ttype in zip(pctors_with_args, named_ttypes)))).replace('\n', '\n' + indent1))
-
-retcode += addnewline((r"""%sDefinition to_typed {t} (idc : ident t) (evm : EvarMap) : type_of_list (arg_types idc) -> %sident.ident (pattern.type.subst_default t evm)
- := match idc in ident t return type_of_list (arg_types idc) -> %sident.ident (pattern.type.subst_default t evm) with
- | %s
- end.
-""" % (indent1, prefix, prefix,
- '\n | '.join('@' + pctor + ' => '
- + make_fun_project_list(ctype, ctor)
- + '@' + ' '.join([ctor[0]] + ['_' for _ in ctor[1:len(ctor)-len(ctype)]] + ctor[len(ctor)-len(ctype):])
- for pctor, ctor, ctype in zip(pctors_with_args, ctors_with_prefix, ctypes)))).replace('\n', '\n' + indent1))
-
-assert(ctors[0][0] == 'ident.Literal')
-assert(len(ctypes[0]) == 1)
-
-retcode += addnewline((r"""%sDefinition unify {t t'} (pidc : ident t) (idc : %sident.ident t') : Datatypes.option (type_of_list (@arg_types t pidc))
- := match pidc, idc return Datatypes.option (type_of_list (arg_types pidc)) with
- | %s
- | %s
- | %s
- => Datatypes.None
- end%%cps.
-""" % (indent1, prefix,
- '\n | '.join('@' + pctor + ' ' + ty + ', ' + ' '.join([ctor[0], ty] + ctor[2:]) + ' => Datatypes.Some ' + fold_right_pair(ctor[-len(ctype):])
- for pctor, ctor, ctype in zip(pctors[:1], ctors_with_prefix[:1], ctypes[:1])
- for ty in base_types),
- '\n | '.join('@' + pctor + ', ' + ' '.join([ctor[0]] + [i + "'" for i in ctor[1:]]) + ' => Datatypes.Some ' + ('tt' if len(ctype) == 0 else fold_right_pair([i + "'" for i in ctor[-len(ctype):]]))
- for pctor, ctor, ctype in zip(pctors_with_args[1:], ctors_with_prefix[1:], ctypes[1:])),
- '\n | '.join('@' + pctor + ', _' for pctor, named_ttype in zip(pctors_with_underscores, named_ttypes)))).replace('\n', '\n' + indent1))
-
-def relax_type_var(name, ty):
- ty = ty.replace(prefix, '')
- return ({'base.type.base': name,
- 'base.type': '(base.relax %s)' % name,
- 'type': '(type.relax %s)' % name,
- 'type.type base.type': '(type.relax %s)' % name})[ty]
-
-retcode += addnewline((r"""%sDefinition of_typed_ident {t} (idc : %sident.ident t) : ident (type.relax t)
- := match idc with
- | %s
- end.
-""" % (indent1, prefix, '\n | '.join(' '.join(ctor) + ' => @' + pctor + ' ' + ' '.join(relax_type_var(n, t) for n, t in named_ttype) for ctor, pctor, named_ttype in zip(ctors_with_prefix, pctors, named_ttypes)))).replace('\n', '\n' + indent1))
-
-retcode += addnewline((r"""%sDefinition arg_types_of_typed_ident {t} (idc : %sident.ident t) : type_of_list (arg_types (of_typed_ident idc))
- := match idc in %sident.ident t return type_of_list (arg_types (of_typed_ident idc)) with
- | %s
- end.
-""" % (indent1, prefix, prefix,
- '\n | '.join(' '.join(ctor) + ' => ' + ('tt' if len(ctype) == 0 else fold_right_pair(ctor[-len(ctype):]))
- for ctor, ctype in zip(ctors_with_prefix, ctypes)))).replace('\n', '\n' + indent1))
-
-
-#
-#
-#retcode += addnewline((r"""%sDefinition retype_ident {t} (idc : %sident.ident t) : match arg_types (of_typed_ident idc) return %s with Datatypes.Some t => t | Datatypes.None => unit end -> %sident.ident t
-# := match idc in %sident.ident t return match arg_types (of_typed_ident idc) return %s with Datatypes.Some t => t | Datatypes.None => unit end -> %sident.ident t with
-# | %s
-# end.
-#""" % (indent1, prefix, type_or_set, prefix, prefix, type_or_set, prefix,
-# '\n | '.join(' '.join(ctor) + ' => '
-# + ('' if not do_adjust_type(ctor, ctype) else '(')
-# + 'fun ' + ('_ => ' if len(ctype) == 0 else ((ctor[-1] + ' => ') if len(ctype) == 1 else "arg => let '(%s) := eta%d arg in " % (', '.join(ctor[-len(ctype):]), len(ctype)))) + "@" + ' '.join(ctor)
-# + ('' if not do_adjust_type(ctor, ctype) else
-# (') : '
-# + ('match arg_types (of_typed_ident %s) return %s with Datatypes.Some t => t | Datatypes.None => unit end -> _'
-# % (('%s' if ' ' not in ' '.join(ctor) else '(@%s)') % ' '.join(ctor),
-# type_or_set))
-# + ' (* COQBUG(https://github.com/coq/coq/issues/7726) *)'))
-# for ctor, ctype in zip(ctors_with_prefix, ctypes)))).replace('\n', '\n' + indent1))
-
-
-
-
-#retcode += addnewline((r"""%sDefinition try_make_transport_ident_cps (P : ident -> Type) (idc1 idc2 : ident) : ~> Datatypes.option (P idc1 -> P idc2)
-# := match idc1, idc2 with
-# | %s
-# => fun T k => k (Datatypes.Some (fun v => v))
-# | %s
-# => fun T k => k Datatypes.None
-# end%%cps.
-#""" % (indent2,
-# '\n | '.join(pctor + ', ' + pctor for pctor in pctors),
-# '\n | '.join(pctor + ', _' for pctor in pctors))).replace('\n', '\n' + indent2))
-#retcode += addnewline((r"""%sDefinition eta_all_option_cps {T} (f : ident -> Datatypes.option T)
-# : Datatypes.option (ident -> T)
-# := (%s;
-# Datatypes.Some (fun c
-# => match c with
-# | %s
-# end))%%option.
-#""" % (indent2,
-# ';\n '.join('f' + pctor + ' <- f ' + ctor[0] for ctor, pctor in zip(ctors_no_prefix, pctors)),
-# '\n | '.join(ctor[0] + ' => f' + pctor for pctor, ctor in zip(pctors, ctors_no_prefix)))).replace('\n', '\n' + indent2))
-#retcode += addnewline((r"""%sDefinition orb (f : ident -> bool) : bool
-# := (%s)%%bool.
-#""" % (indent2, ' || '.join('f ' + pctor for pctor in pctors))).replace('\n', '\n' + indent2))
-
-#retcode += addnewline((r"""%sDefinition bind_args {t} (idc : %sident.ident t) : type_of_list (arg_types (of_typed_ident idc))
-# := match idc return type_of_list (arg_types (of_typed_ident idc)) with
-# | %s
-# end%%cps.
-#""" % (indent1, prefix,
-# '\n | '.join(' '.join(ctor) + ' => ' + ('tt' if len(ttype + ctype) == 0 else fold_right_pair(ctor[-len(ttype + ctype):]))
-# for ctor, ttype, ctype in zip(ctors_with_prefix, ttypes, ctypes)))).replace('\n', '\n' + indent1))
-#maxeta = max([1+len(ttype + ctype) for ttype, ctype in zip(ttypes, ctypes)])
-#if maxeta >= 2:
-# retcode += addnewline(r"""%sLocal Notation eta2r x := (Datatypes.fst x, Datatypes.snd x) (only parsing).""" % indent1)
-#for i in range(3, maxeta+1):
-# retcode += addnewline(r"""%sLocal Notation eta%dr x := (Datatypes.fst x, eta%dr (Datatypes.snd x)) (only parsing).""" % (indent1, i, i-1))
-#retcode += addnewline('')
-#
-#def do_adjust_type(ctor, ctype):
-# return len(ctor) > 1 and 'Literal' in ctor[0]
-#
-#retcode += addnewline((r"""%sDefinition type_of (pidc : ident) : type_of_list (arg_types pidc) -> %stype %sbase.type
-# := match pidc return type_of_list (arg_types pidc) -> _ with
-# | %s
-# end%%etype.
-#""" % (indent1, prefix, prefix,
-# '\n | '.join(pctor + ' => '
-# + 'fun ' + ('_ => ' if len(ttype + ctype) == 0 else "arg => let '%s := eta%dr arg in " % (fold_right_pair(ctor[-len(ttype + ctype):], tt='_'), 1+len(ttype + ctype))) + cretty.replace(prefix + 'ident.ident ', '')
-# for pctor, ctor, ttype, ctype, cretty in zip(pctors, ctors_with_prefix, ttypes, ctypes, crettypes)))).replace('\n', '\n' + indent1))
-#retcode += addnewline((r"""%sDefinition to_typed (pidc : ident) : forall args : type_of_list (arg_types pidc), %sident.ident (type_of pidc args)
-# := match pidc return forall args : type_of_list (arg_types pidc), %sident.ident (type_of pidc args) with
-# | %s
-# end.
-#""" % (indent1, prefix, prefix,
-# '\n | '.join(pctor + ' => '
-# + 'fun ' + (('_ => %s' if len(ttype + ctype) == 0 else "arg => match eta%dr arg as args' return %sident.ident (type_of %s args') with %s => %%s end" % (1+len(ttype + ctype), prefix, pctor, fold_right_pair(ctor[-len(ttype + ctype):], tt='_'))) % ("@" + ' '.join(ctor)))
-# for pctor, ctor, ttype, ctype in zip(pctors, ctors_with_prefix, ttypes, ctypes)))).replace('\n', '\n' + indent1))
-
-
-
-retcode += r""" Derive type_of_list_arg_types_beq
- SuchThat (forall {t idc}, reflect_rel (@eq (type_of_list (@arg_types t idc))) (@type_of_list_arg_types_beq t idc))
- As reflect_type_of_list_arg_types_beq.
- Proof.
- subst type_of_list_arg_types_beq; intros t idc.
- instantiate (1:=ltac:(intros t idc; destruct idc)); destruct idc; cbn [fold_right arg_types]; try solve [ exact reflect_eq_unit ]; instantiate (1:=ltac:(cbn [fold_right arg_types])); exact _.
- Qed.
-"""
-
-
-retcode += r""" End ident.
-"""
-
-retcode += addnewline(indent0 + '\n' + indent0 + '(*===*)')
-retcode += r"""
- End pattern.
-End Compilers.
-"""
-with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
- f.write(retcode)
-
->>>
- *)
-
- Local Notation eta2 x := (Datatypes.fst x, Datatypes.snd x) (only parsing).
- Local Notation eta2r x := (Datatypes.fst x, Datatypes.snd x) (only parsing).
- Local Notation eta3 x := (eta2 (Datatypes.fst x), Datatypes.snd x) (only parsing).
- Local Notation eta3r x := (Datatypes.fst x, eta2r (Datatypes.snd x)) (only parsing).
-
+ Module Import Tactics.
+ Ltac build_all_idents_gen P :=
+ let idc' := fresh "idc'" in
+ let res := open_constr:(_ : list { T : Type & T }) in
+ let fill_next v :=
+ let next := match res with
+ | context[?ev]
+ => let __ := match goal with _ => is_evar ev end in
+ ev
+ end in
+ let __ := open_constr:(eq_refl : next = v) in
+ constr:(I) in
+ let __ := open_constr:(
+ ltac:(intros;
+ lazymatch goal with
+ | [ idc : _ |- _ ] => pose idc as idc'; destruct idc
+ end;
+ let idc := (eval cbv [idc'] in idc') in
+ let h := head idc in
+ let __ := fill_next open_constr:(Datatypes.cons (existT (fun T => T) _ h) _) in
+ constructor)
+ : P) in
+ let __ := fill_next uconstr:(Datatypes.nil) in
+ res.
+ Ltac build_all_idents := build_all_idents_gen (forall t (idc : Compilers.ident.ident t), True).
+ Ltac make_all_idents := let v := build_all_idents in refine v.
+
+ Ltac strip_default v :=
+ let v := lazymatch v with
+ | (fun _ => ?v) => v
+ | _ => constr_fail_with ltac:(fun _ => fail 1 "Could not eliminate dependency on dummy default argument in" v)
+ end in
+ v.
+ Ltac strip2_args v :=
+ let v := lazymatch v with
+ | (fun _ _ => ?v) => v
+ | _ => constr_fail_with ltac:(fun _ => fail 1 "Could not eliminate dependency on first two dummy arguments in" v)
+ end in
+ v.
+
+ Ltac make_eta_ident_cps_gen_gen do_destruct_base :=
+ unshelve eexists; intros;
+ lazymatch goal with idc : _ |- _ => destruct idc end;
+ lazymatch do_destruct_base with
+ | true => repeat match goal with t : base.type.base |- _ => destruct t end
+ | false => idtac
+ end;
+ shelve_unifiable; reflexivity.
+ Ltac make_eta_ident_cps_gen := make_eta_ident_cps_gen_gen false.
+ Ltac make_eta_ident_cps_gen_expand_literal := make_eta_ident_cps_gen_gen true.
+
+ Ltac get_ctor_number' ctor all_idents :=
+ lazymatch all_idents with
+ | Datatypes.cons ctor _ => Datatypes.O
+ | Datatypes.cons (existT _ _ ctor) _ => Datatypes.O
+ | Datatypes.cons _ ?xs => let v := get_ctor_number' ctor xs in
+ constr:(Datatypes.S v)
+ end.
+
+ Ltac find_ctor ctor from_all_idents to_all_idents :=
+ let n := get_ctor_number' ctor from_all_idents in
+ let v := (eval cbv [List.nth] in (fun default => List.nth n to_all_idents default)) in
+ let v := lazymatch v with
+ | (fun _ => ?v) => v
+ | _ => 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.
+ End Tactics.
+
+ Definition all_idents : list { T : Type & T } := ltac:(make_all_idents).
+
+ Definition eta_ident_cps_gen
+ {T : forall t, Compilers.ident.ident t -> Type}
+ (f : forall t idc, T t idc)
+ : { f' : forall t idc, T t idc | forall t idc, f' t idc = f t idc }.
+ Proof. make_eta_ident_cps_gen. Defined.
+
+ Definition eta_ident_cps_gen_expand_literal
+ {T : forall t, Compilers.ident.ident t -> Type}
+ (f : forall t idc, T t idc)
+ : { f' : forall t idc, T t idc | forall t idc, f' t idc = f t idc }.
+ Proof. make_eta_ident_cps_gen_expand_literal. Defined.
+
+ 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}
+ (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.
+
+ 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}
+ (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.
Module Raw.
Module ident.
+ Local Unset Decidable Equality Schemes.
+ Module MakeIdent.
+ Import Compilers.ident.
+ Ltac map_projT2 tac ls :=
+ lazymatch ls with
+ | Datatypes.nil => idtac
+ | Datatypes.cons (existT _ _ ?v) ?ls
+ => tac v; map_projT2 tac ls
+ end.
+ Ltac fill_forall_args v :=
+ let T := type of v in
+ lazymatch (eval cbv beta in T) with
+ | ?A -> ?B => v
+ | forall x : ?A, _ => fill_forall_args open_constr:(v _)
+ | _ => v
+ end.
+ Ltac print_ident :=
+ idtac " Inductive ident :=";
+ let v := (eval cbv [pattern.all_idents] in pattern.all_idents) in
+ map_projT2 ltac:(fun v => let v := fill_forall_args v in idtac " |" v) v;
+ idtac " .".
+ Local Unset Printing Notations.
+ (*Goal True. print_ident. Abort.*)
+ End MakeIdent.
Inductive ident :=
| Literal
| Nat_succ
@@ -1586,1491 +381,775 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
| fancy_selc
| fancy_selm
| fancy_sell
- | fancy_addm.
-
- Definition full_types (idc : ident) : Type
- := match idc return Type with
- | Literal => { t : base.type.base & base.interp (Compilers.base.type.type_base t) }
- | Nat_succ => unit
- | Nat_pred => unit
- | Nat_max => unit
- | Nat_mul => unit
- | Nat_add => unit
- | Nat_sub => unit
- | Nat_eqb => unit
- | nil => Compilers.base.type
- | cons => Compilers.base.type
- | pair => Compilers.base.type * Compilers.base.type
- | fst => Compilers.base.type * Compilers.base.type
- | snd => Compilers.base.type * Compilers.base.type
- | prod_rect => Compilers.base.type * Compilers.base.type * Compilers.base.type
- | bool_rect => Compilers.base.type
- | nat_rect => Compilers.base.type
- | nat_rect_arrow => Compilers.base.type * Compilers.base.type
- | 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
- | List_length => Compilers.base.type
- | List_seq => unit
- | List_firstn => Compilers.base.type
- | List_skipn => Compilers.base.type
- | List_repeat => Compilers.base.type
- | List_combine => Compilers.base.type * Compilers.base.type
- | List_map => Compilers.base.type * Compilers.base.type
- | List_app => Compilers.base.type
- | List_rev => Compilers.base.type
- | List_flat_map => Compilers.base.type * Compilers.base.type
- | List_partition => Compilers.base.type
- | List_fold_right => Compilers.base.type * Compilers.base.type
- | List_update_nth => Compilers.base.type
- | List_nth_default => Compilers.base.type
- | eager_List_nth_default => Compilers.base.type
- | Z_add => unit
- | Z_mul => unit
- | Z_pow => unit
- | Z_sub => unit
- | Z_opp => unit
- | Z_div => unit
- | Z_modulo => unit
- | Z_log2 => unit
- | Z_log2_up => unit
- | Z_eqb => unit
- | Z_leb => unit
- | Z_ltb => unit
- | Z_geb => unit
- | Z_gtb => unit
- | Z_of_nat => unit
- | Z_to_nat => unit
- | Z_shiftr => unit
- | Z_shiftl => unit
- | Z_land => unit
- | Z_lor => unit
- | Z_min => unit
- | Z_max => unit
- | Z_bneg => unit
- | Z_lnot_modulo => unit
- | Z_mul_split => unit
- | Z_add_get_carry => unit
- | Z_add_with_carry => unit
- | Z_add_with_get_carry => unit
- | Z_sub_get_borrow => unit
- | Z_sub_with_get_borrow => unit
- | Z_zselect => unit
- | Z_add_modulo => unit
- | Z_rshi => unit
- | Z_cc_m => unit
- | Z_combine_at_bitwidth => unit
- | Z_cast => zrange
- | Z_cast2 => zrange * zrange
- | option_Some => Compilers.base.type
- | option_None => Compilers.base.type
- | option_rect => Compilers.base.type * Compilers.base.type
- | Build_zrange => unit
- | zrange_rect => Compilers.base.type
- | fancy_add => Z * Z
- | fancy_addc => Z * Z
- | fancy_sub => Z * Z
- | fancy_subb => Z * Z
- | fancy_mulll => Z
- | fancy_mullh => Z
- | fancy_mulhl => Z
- | fancy_mulhh => Z
- | fancy_rshi => Z * Z
- | fancy_selc => unit
- | fancy_selm => Z
- | fancy_sell => unit
- | fancy_addm => unit
- end%type.
-
- Definition is_simple (idc : ident) : bool
- := match idc with
- | Literal => false
- | Nat_succ => true
- | Nat_pred => true
- | Nat_max => true
- | Nat_mul => true
- | Nat_add => true
- | Nat_sub => true
- | Nat_eqb => true
- | nil => false
- | cons => false
- | pair => false
- | fst => false
- | snd => false
- | prod_rect => false
- | bool_rect => false
- | nat_rect => false
- | nat_rect_arrow => false
- | 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
- | List_length => false
- | List_seq => true
- | List_firstn => false
- | List_skipn => false
- | List_repeat => false
- | List_combine => false
- | List_map => false
- | List_app => false
- | List_rev => false
- | List_flat_map => false
- | List_partition => false
- | List_fold_right => false
- | List_update_nth => false
- | List_nth_default => false
- | eager_List_nth_default => false
- | Z_add => true
- | Z_mul => true
- | Z_pow => true
- | Z_sub => true
- | Z_opp => true
- | Z_div => true
- | Z_modulo => true
- | Z_log2 => true
- | Z_log2_up => true
- | Z_eqb => true
- | Z_leb => true
- | Z_ltb => true
- | Z_geb => true
- | Z_gtb => true
- | Z_of_nat => true
- | Z_to_nat => true
- | Z_shiftr => true
- | Z_shiftl => true
- | Z_land => true
- | Z_lor => true
- | Z_min => true
- | Z_max => true
- | Z_bneg => true
- | Z_lnot_modulo => true
- | Z_mul_split => true
- | Z_add_get_carry => true
- | Z_add_with_carry => true
- | Z_add_with_get_carry => true
- | Z_sub_get_borrow => true
- | Z_sub_with_get_borrow => true
- | Z_zselect => true
- | Z_add_modulo => true
- | Z_rshi => true
- | Z_cc_m => true
- | Z_combine_at_bitwidth => true
- | Z_cast => true
- | Z_cast2 => true
- | option_Some => false
- | option_None => false
- | option_rect => false
- | Build_zrange => true
- | zrange_rect => false
- | fancy_add => true
- | fancy_addc => true
- | fancy_sub => true
- | fancy_subb => true
- | fancy_mulll => true
- | fancy_mullh => true
- | fancy_mulhl => true
- | fancy_mulhh => true
- | fancy_rshi => true
- | fancy_selc => true
- | fancy_selm => true
- | fancy_sell => true
- | fancy_addm => true
- end.
-
- Definition invert_bind_args {t} (idc : Compilers.ident.ident t) (pidc : ident) : Datatypes.option (full_types pidc)
- := match pidc, idc return Datatypes.option (full_types pidc) with
- | Literal, Compilers.ident.Literal t v => Datatypes.Some (existT _ t v)
- | Nat_succ, Compilers.ident.Nat_succ => Datatypes.Some tt
- | Nat_pred, Compilers.ident.Nat_pred => Datatypes.Some tt
- | Nat_max, Compilers.ident.Nat_max => Datatypes.Some tt
- | Nat_mul, Compilers.ident.Nat_mul => Datatypes.Some tt
- | Nat_add, Compilers.ident.Nat_add => Datatypes.Some tt
- | Nat_sub, Compilers.ident.Nat_sub => Datatypes.Some tt
- | Nat_eqb, Compilers.ident.Nat_eqb => Datatypes.Some tt
- | nil, Compilers.ident.nil t => Datatypes.Some t
- | cons, Compilers.ident.cons t => Datatypes.Some t
- | pair, Compilers.ident.pair A B => Datatypes.Some (A, B)
- | fst, Compilers.ident.fst A B => Datatypes.Some (A, B)
- | snd, Compilers.ident.snd A B => Datatypes.Some (A, B)
- | prod_rect, Compilers.ident.prod_rect A B T => Datatypes.Some (A, B, T)
- | bool_rect, Compilers.ident.bool_rect T => Datatypes.Some T
- | nat_rect, Compilers.ident.nat_rect P => Datatypes.Some P
- | nat_rect_arrow, Compilers.ident.nat_rect_arrow P Q => Datatypes.Some (P, Q)
- | 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)
- | List_length, Compilers.ident.List_length T => Datatypes.Some T
- | List_seq, Compilers.ident.List_seq => Datatypes.Some tt
- | List_firstn, Compilers.ident.List_firstn A => Datatypes.Some A
- | List_skipn, Compilers.ident.List_skipn A => Datatypes.Some A
- | List_repeat, Compilers.ident.List_repeat A => Datatypes.Some A
- | List_combine, Compilers.ident.List_combine A B => Datatypes.Some (A, B)
- | List_map, Compilers.ident.List_map A B => Datatypes.Some (A, B)
- | List_app, Compilers.ident.List_app A => Datatypes.Some A
- | List_rev, Compilers.ident.List_rev A => Datatypes.Some A
- | List_flat_map, Compilers.ident.List_flat_map A B => Datatypes.Some (A, B)
- | List_partition, Compilers.ident.List_partition A => Datatypes.Some A
- | List_fold_right, Compilers.ident.List_fold_right A B => Datatypes.Some (A, B)
- | List_update_nth, Compilers.ident.List_update_nth T => Datatypes.Some T
- | List_nth_default, Compilers.ident.List_nth_default T => Datatypes.Some T
- | eager_List_nth_default, Compilers.ident.eager_List_nth_default T => Datatypes.Some T
- | Z_add, Compilers.ident.Z_add => Datatypes.Some tt
- | Z_mul, Compilers.ident.Z_mul => Datatypes.Some tt
- | Z_pow, Compilers.ident.Z_pow => Datatypes.Some tt
- | Z_sub, Compilers.ident.Z_sub => Datatypes.Some tt
- | Z_opp, Compilers.ident.Z_opp => Datatypes.Some tt
- | Z_div, Compilers.ident.Z_div => Datatypes.Some tt
- | Z_modulo, Compilers.ident.Z_modulo => Datatypes.Some tt
- | Z_log2, Compilers.ident.Z_log2 => Datatypes.Some tt
- | Z_log2_up, Compilers.ident.Z_log2_up => Datatypes.Some tt
- | Z_eqb, Compilers.ident.Z_eqb => Datatypes.Some tt
- | Z_leb, Compilers.ident.Z_leb => Datatypes.Some tt
- | Z_ltb, Compilers.ident.Z_ltb => Datatypes.Some tt
- | Z_geb, Compilers.ident.Z_geb => Datatypes.Some tt
- | Z_gtb, Compilers.ident.Z_gtb => Datatypes.Some tt
- | Z_of_nat, Compilers.ident.Z_of_nat => Datatypes.Some tt
- | Z_to_nat, Compilers.ident.Z_to_nat => Datatypes.Some tt
- | Z_shiftr, Compilers.ident.Z_shiftr => Datatypes.Some tt
- | Z_shiftl, Compilers.ident.Z_shiftl => Datatypes.Some tt
- | Z_land, Compilers.ident.Z_land => Datatypes.Some tt
- | Z_lor, Compilers.ident.Z_lor => Datatypes.Some tt
- | Z_min, Compilers.ident.Z_min => Datatypes.Some tt
- | Z_max, Compilers.ident.Z_max => Datatypes.Some tt
- | Z_bneg, Compilers.ident.Z_bneg => Datatypes.Some tt
- | Z_lnot_modulo, Compilers.ident.Z_lnot_modulo => Datatypes.Some tt
- | Z_mul_split, Compilers.ident.Z_mul_split => Datatypes.Some tt
- | Z_add_get_carry, Compilers.ident.Z_add_get_carry => Datatypes.Some tt
- | Z_add_with_carry, Compilers.ident.Z_add_with_carry => Datatypes.Some tt
- | Z_add_with_get_carry, Compilers.ident.Z_add_with_get_carry => Datatypes.Some tt
- | Z_sub_get_borrow, Compilers.ident.Z_sub_get_borrow => Datatypes.Some tt
- | Z_sub_with_get_borrow, Compilers.ident.Z_sub_with_get_borrow => Datatypes.Some tt
- | Z_zselect, Compilers.ident.Z_zselect => Datatypes.Some tt
- | Z_add_modulo, Compilers.ident.Z_add_modulo => Datatypes.Some tt
- | Z_rshi, Compilers.ident.Z_rshi => Datatypes.Some tt
- | Z_cc_m, Compilers.ident.Z_cc_m => Datatypes.Some tt
- | Z_combine_at_bitwidth, Compilers.ident.Z_combine_at_bitwidth => Datatypes.Some tt
- | Z_cast, Compilers.ident.Z_cast range => Datatypes.Some range
- | Z_cast2, Compilers.ident.Z_cast2 range => Datatypes.Some range
- | option_Some, Compilers.ident.option_Some A => Datatypes.Some A
- | option_None, Compilers.ident.option_None A => Datatypes.Some A
- | option_rect, Compilers.ident.option_rect A P => Datatypes.Some (A, P)
- | Build_zrange, Compilers.ident.Build_zrange => Datatypes.Some tt
- | zrange_rect, Compilers.ident.zrange_rect P => Datatypes.Some P
- | fancy_add, Compilers.ident.fancy_add log2wordmax imm => Datatypes.Some (log2wordmax, imm)
- | fancy_addc, Compilers.ident.fancy_addc log2wordmax imm => Datatypes.Some (log2wordmax, imm)
- | fancy_sub, Compilers.ident.fancy_sub log2wordmax imm => Datatypes.Some (log2wordmax, imm)
- | fancy_subb, Compilers.ident.fancy_subb log2wordmax imm => Datatypes.Some (log2wordmax, imm)
- | fancy_mulll, Compilers.ident.fancy_mulll log2wordmax => Datatypes.Some log2wordmax
- | fancy_mullh, Compilers.ident.fancy_mullh log2wordmax => Datatypes.Some log2wordmax
- | fancy_mulhl, Compilers.ident.fancy_mulhl log2wordmax => Datatypes.Some log2wordmax
- | fancy_mulhh, Compilers.ident.fancy_mulhh log2wordmax => Datatypes.Some log2wordmax
- | fancy_rshi, Compilers.ident.fancy_rshi log2wordmax x => Datatypes.Some (log2wordmax, x)
- | fancy_selc, Compilers.ident.fancy_selc => Datatypes.Some tt
- | fancy_selm, Compilers.ident.fancy_selm log2wordmax => Datatypes.Some log2wordmax
- | fancy_sell, Compilers.ident.fancy_sell => Datatypes.Some tt
- | fancy_addm, Compilers.ident.fancy_addm => Datatypes.Some tt
- | Literal, _
- | Nat_succ, _
- | Nat_pred, _
- | Nat_max, _
- | Nat_mul, _
- | Nat_add, _
- | Nat_sub, _
- | Nat_eqb, _
- | nil, _
- | cons, _
- | pair, _
- | fst, _
- | snd, _
- | prod_rect, _
- | bool_rect, _
- | nat_rect, _
- | nat_rect_arrow, _
- | eager_nat_rect, _
- | eager_nat_rect_arrow, _
- | list_rect, _
- | list_rect_arrow, _
- | eager_list_rect, _
- | eager_list_rect_arrow, _
- | list_case, _
- | List_length, _
- | List_seq, _
- | List_firstn, _
- | List_skipn, _
- | List_repeat, _
- | List_combine, _
- | List_map, _
- | List_app, _
- | List_rev, _
- | List_flat_map, _
- | List_partition, _
- | List_fold_right, _
- | List_update_nth, _
- | List_nth_default, _
- | eager_List_nth_default, _
- | Z_add, _
- | Z_mul, _
- | Z_pow, _
- | Z_sub, _
- | Z_opp, _
- | Z_div, _
- | Z_modulo, _
- | Z_log2, _
- | Z_log2_up, _
- | Z_eqb, _
- | Z_leb, _
- | Z_ltb, _
- | Z_geb, _
- | Z_gtb, _
- | Z_of_nat, _
- | Z_to_nat, _
- | Z_shiftr, _
- | Z_shiftl, _
- | Z_land, _
- | Z_lor, _
- | Z_min, _
- | Z_max, _
- | Z_bneg, _
- | Z_lnot_modulo, _
- | Z_mul_split, _
- | Z_add_get_carry, _
- | Z_add_with_carry, _
- | Z_add_with_get_carry, _
- | Z_sub_get_borrow, _
- | Z_sub_with_get_borrow, _
- | Z_zselect, _
- | Z_add_modulo, _
- | Z_rshi, _
- | Z_cc_m, _
- | Z_combine_at_bitwidth, _
- | Z_cast, _
- | Z_cast2, _
- | option_Some, _
- | option_None, _
- | option_rect, _
- | Build_zrange, _
- | zrange_rect, _
- | fancy_add, _
- | fancy_addc, _
- | fancy_sub, _
- | fancy_subb, _
- | fancy_mulll, _
- | fancy_mullh, _
- | fancy_mulhl, _
- | fancy_mulhh, _
- | fancy_rshi, _
- | fancy_selc, _
- | fancy_selm, _
- | fancy_sell, _
- | fancy_addm, _
- => Datatypes.None
- end%cps.
-
- Definition type_of (pidc : ident) : full_types pidc -> Compilers.type Compilers.base.type
- := match pidc return full_types pidc -> _ with
- | Literal => fun arg => let '(t, v) := (projT1 arg, projT2 arg) in (type.base (Compilers.base.type.type_base t))
- | Nat_succ => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
- | Nat_pred => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
- | Nat_max => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
- | Nat_mul => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
- | Nat_add => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
- | Nat_sub => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
- | Nat_eqb => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.bool))%ptype
- | nil => fun t => (type.base (Compilers.base.type.list t))
- | cons => fun t => (type.base t -> type.base (Compilers.base.type.list t) -> type.base (Compilers.base.type.list t))%ptype
- | pair => fun arg => let '(A, B) := eta2 arg in (type.base A -> type.base B -> type.base (A * B)%etype)%ptype
- | fst => fun arg => let '(A, B) := eta2 arg in (type.base (A * B)%etype -> type.base A)%ptype
- | snd => fun arg => let '(A, B) := eta2 arg in (type.base (A * B)%etype -> type.base B)%ptype
- | prod_rect => fun arg => let '(A, B, T) := eta3 arg in ((type.base A -> type.base B -> type.base T) -> type.base (A * B)%etype -> type.base T)%ptype
- | bool_rect => fun T => ((type.base ()%etype -> type.base T) -> (type.base ()%etype -> type.base T) -> type.base (Compilers.base.type.type_base base.type.bool) -> type.base T)%ptype
- | 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
- | 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
- | 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
- | List_length => fun T => (type.base (Compilers.base.type.list T) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
- | List_seq => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.list (Compilers.base.type.type_base base.type.nat)))%ptype
- | List_firstn => fun A => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list A))%ptype
- | List_skipn => fun A => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list A))%ptype
- | List_repeat => fun A => (type.base A -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.list A))%ptype
- | List_combine => fun arg => let '(A, B) := eta2 arg in (type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list B) -> type.base (Compilers.base.type.list (A * B)))%ptype
- | List_map => fun arg => let '(A, B) := eta2 arg in ((type.base A -> type.base B) -> type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list B))%ptype
- | List_app => fun A => (type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list A))%ptype
- | List_rev => fun A => (type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list A))%ptype
- | List_flat_map => fun arg => let '(A, B) := eta2 arg in ((type.base A -> type.base (Compilers.base.type.list B)) -> type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list B))%ptype
- | List_partition => fun A => ((type.base A -> type.base (Compilers.base.type.type_base base.type.bool)) -> type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list A * Compilers.base.type.list A)%etype)%ptype
- | List_fold_right => fun arg => let '(A, B) := eta2 arg in ((type.base B -> type.base A -> type.base A) -> type.base A -> type.base (Compilers.base.type.list B) -> type.base A)%ptype
- | List_update_nth => fun T => (type.base (Compilers.base.type.type_base base.type.nat) -> (type.base T -> type.base T) -> type.base (Compilers.base.type.list T) -> type.base (Compilers.base.type.list T))%ptype
- | List_nth_default => fun T => (type.base T -> type.base (Compilers.base.type.list T) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base T)%ptype
- | eager_List_nth_default => fun T => (type.base T -> type.base (Compilers.base.type.list T) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base T)%ptype
- | Z_add => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_mul => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_pow => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_sub => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_opp => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_div => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_modulo => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_log2 => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_log2_up => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_eqb => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.bool))%ptype
- | Z_leb => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.bool))%ptype
- | Z_ltb => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.bool))%ptype
- | Z_geb => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.bool))%ptype
- | Z_gtb => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.bool))%ptype
- | Z_of_nat => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_to_nat => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.nat))%ptype
- | Z_shiftr => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_shiftl => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_land => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_lor => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_min => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_max => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_bneg => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_lnot_modulo => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_mul_split => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | Z_add_get_carry => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | Z_add_with_carry => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_add_with_get_carry => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | Z_sub_get_borrow => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | Z_sub_with_get_borrow => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | Z_zselect => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_add_modulo => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_rshi => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_cc_m => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_combine_at_bitwidth => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_cast => fun range => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | Z_cast2 => fun range => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | option_Some => fun A => (type.base A -> type.base (Compilers.base.type.option A))%ptype
- | option_None => fun A => (type.base (Compilers.base.type.option A))
- | option_rect => fun arg => let '(A, P) := eta2 arg in ((type.base A -> type.base P) -> (type.base ()%etype -> type.base P) -> type.base (Compilers.base.type.option A) -> type.base P)%ptype
- | Build_zrange => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.zrange))%ptype
- | zrange_rect => fun P => ((type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z) -> type.base P) -> type.base (Compilers.base.type.type_base base.type.zrange) -> type.base P)%ptype
- | fancy_add => fun arg => let '(log2wordmax, imm) := eta2 arg in (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | fancy_addc => fun arg => let '(log2wordmax, imm) := eta2 arg in (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | fancy_sub => fun arg => let '(log2wordmax, imm) := eta2 arg in (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | fancy_subb => fun arg => let '(log2wordmax, imm) := eta2 arg in (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%ptype
- | fancy_mulll => fun log2wordmax => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_mullh => fun log2wordmax => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_mulhl => fun log2wordmax => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_mulhh => fun log2wordmax => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_rshi => fun arg => let '(log2wordmax, x) := eta2 arg in (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_selc => fun _ => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_selm => fun log2wordmax => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_sell => fun _ => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- | fancy_addm => fun _ => (type.base (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype -> type.base (Compilers.base.type.type_base base.type.Z))%ptype
- end%etype.
-
- Definition to_typed (pidc : ident) : forall args : full_types pidc, Compilers.ident.ident (type_of pidc args)
- := match pidc return forall args : full_types pidc, Compilers.ident.ident (type_of pidc args) with
- | Literal => fun arg => match existT _ (projT1 arg) (projT2 arg) as arg' return Compilers.ident.ident (type_of Literal arg') with existT t v => @Compilers.ident.Literal t v end
- | Nat_succ => fun _ => @Compilers.ident.Nat_succ
- | Nat_pred => fun _ => @Compilers.ident.Nat_pred
- | Nat_max => fun _ => @Compilers.ident.Nat_max
- | Nat_mul => fun _ => @Compilers.ident.Nat_mul
- | Nat_add => fun _ => @Compilers.ident.Nat_add
- | Nat_sub => fun _ => @Compilers.ident.Nat_sub
- | Nat_eqb => fun _ => @Compilers.ident.Nat_eqb
- | nil => fun t => @Compilers.ident.nil t
- | cons => fun t => @Compilers.ident.cons t
- | pair => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of pair arg') with (A, B) => @Compilers.ident.pair A B end
- | fst => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of fst arg') with (A, B) => @Compilers.ident.fst A B end
- | snd => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of snd arg') with (A, B) => @Compilers.ident.snd A B end
- | prod_rect => fun arg => match eta3 arg as arg' return Compilers.ident.ident (type_of prod_rect arg') with (A, B, T) => @Compilers.ident.prod_rect A B T end
- | bool_rect => fun T => @Compilers.ident.bool_rect T
- | nat_rect => fun P => @Compilers.ident.nat_rect P
- | nat_rect_arrow => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of nat_rect_arrow arg') with (P, Q) => @Compilers.ident.nat_rect_arrow P Q end
- | 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
- | List_length => fun T => @Compilers.ident.List_length T
- | List_seq => fun _ => @Compilers.ident.List_seq
- | List_firstn => fun A => @Compilers.ident.List_firstn A
- | List_skipn => fun A => @Compilers.ident.List_skipn A
- | List_repeat => fun A => @Compilers.ident.List_repeat A
- | List_combine => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of List_combine arg') with (A, B) => @Compilers.ident.List_combine A B end
- | List_map => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of List_map arg') with (A, B) => @Compilers.ident.List_map A B end
- | List_app => fun A => @Compilers.ident.List_app A
- | List_rev => fun A => @Compilers.ident.List_rev A
- | List_flat_map => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of List_flat_map arg') with (A, B) => @Compilers.ident.List_flat_map A B end
- | List_partition => fun A => @Compilers.ident.List_partition A
- | List_fold_right => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of List_fold_right arg') with (A, B) => @Compilers.ident.List_fold_right A B end
- | List_update_nth => fun T => @Compilers.ident.List_update_nth T
- | List_nth_default => fun T => @Compilers.ident.List_nth_default T
- | eager_List_nth_default => fun T => @Compilers.ident.eager_List_nth_default T
- | Z_add => fun _ => @Compilers.ident.Z_add
- | Z_mul => fun _ => @Compilers.ident.Z_mul
- | Z_pow => fun _ => @Compilers.ident.Z_pow
- | Z_sub => fun _ => @Compilers.ident.Z_sub
- | Z_opp => fun _ => @Compilers.ident.Z_opp
- | Z_div => fun _ => @Compilers.ident.Z_div
- | Z_modulo => fun _ => @Compilers.ident.Z_modulo
- | Z_log2 => fun _ => @Compilers.ident.Z_log2
- | Z_log2_up => fun _ => @Compilers.ident.Z_log2_up
- | Z_eqb => fun _ => @Compilers.ident.Z_eqb
- | Z_leb => fun _ => @Compilers.ident.Z_leb
- | Z_ltb => fun _ => @Compilers.ident.Z_ltb
- | Z_geb => fun _ => @Compilers.ident.Z_geb
- | Z_gtb => fun _ => @Compilers.ident.Z_gtb
- | Z_of_nat => fun _ => @Compilers.ident.Z_of_nat
- | Z_to_nat => fun _ => @Compilers.ident.Z_to_nat
- | Z_shiftr => fun _ => @Compilers.ident.Z_shiftr
- | Z_shiftl => fun _ => @Compilers.ident.Z_shiftl
- | Z_land => fun _ => @Compilers.ident.Z_land
- | Z_lor => fun _ => @Compilers.ident.Z_lor
- | Z_min => fun _ => @Compilers.ident.Z_min
- | Z_max => fun _ => @Compilers.ident.Z_max
- | Z_bneg => fun _ => @Compilers.ident.Z_bneg
- | Z_lnot_modulo => fun _ => @Compilers.ident.Z_lnot_modulo
- | Z_mul_split => fun _ => @Compilers.ident.Z_mul_split
- | Z_add_get_carry => fun _ => @Compilers.ident.Z_add_get_carry
- | Z_add_with_carry => fun _ => @Compilers.ident.Z_add_with_carry
- | Z_add_with_get_carry => fun _ => @Compilers.ident.Z_add_with_get_carry
- | Z_sub_get_borrow => fun _ => @Compilers.ident.Z_sub_get_borrow
- | Z_sub_with_get_borrow => fun _ => @Compilers.ident.Z_sub_with_get_borrow
- | Z_zselect => fun _ => @Compilers.ident.Z_zselect
- | Z_add_modulo => fun _ => @Compilers.ident.Z_add_modulo
- | Z_rshi => fun _ => @Compilers.ident.Z_rshi
- | Z_cc_m => fun _ => @Compilers.ident.Z_cc_m
- | Z_combine_at_bitwidth => fun _ => @Compilers.ident.Z_combine_at_bitwidth
- | Z_cast => fun range => @Compilers.ident.Z_cast range
- | Z_cast2 => fun range => @Compilers.ident.Z_cast2 range
- | option_Some => fun A => @Compilers.ident.option_Some A
- | option_None => fun A => @Compilers.ident.option_None A
- | option_rect => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of option_rect arg') with (A, P) => @Compilers.ident.option_rect A P end
- | Build_zrange => fun _ => @Compilers.ident.Build_zrange
- | zrange_rect => fun P => @Compilers.ident.zrange_rect P
- | fancy_add => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of fancy_add arg') with (log2wordmax, imm) => @Compilers.ident.fancy_add log2wordmax imm end
- | fancy_addc => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of fancy_addc arg') with (log2wordmax, imm) => @Compilers.ident.fancy_addc log2wordmax imm end
- | fancy_sub => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of fancy_sub arg') with (log2wordmax, imm) => @Compilers.ident.fancy_sub log2wordmax imm end
- | fancy_subb => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of fancy_subb arg') with (log2wordmax, imm) => @Compilers.ident.fancy_subb log2wordmax imm end
- | fancy_mulll => fun log2wordmax => @Compilers.ident.fancy_mulll log2wordmax
- | fancy_mullh => fun log2wordmax => @Compilers.ident.fancy_mullh log2wordmax
- | fancy_mulhl => fun log2wordmax => @Compilers.ident.fancy_mulhl log2wordmax
- | fancy_mulhh => fun log2wordmax => @Compilers.ident.fancy_mulhh log2wordmax
- | fancy_rshi => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of fancy_rshi arg') with (log2wordmax, x) => @Compilers.ident.fancy_rshi log2wordmax x end
- | fancy_selc => fun _ => @Compilers.ident.fancy_selc
- | fancy_selm => fun log2wordmax => @Compilers.ident.fancy_selm log2wordmax
- | fancy_sell => fun _ => @Compilers.ident.fancy_sell
- | fancy_addm => fun _ => @Compilers.ident.fancy_addm
+ | fancy_addm
+ .
+
+ Module Import Tactics.
+ Ltac map_projT2 ls :=
+ lazymatch eval cbv beta in ls with
+ | Datatypes.nil => uconstr:(Datatypes.nil)
+ | Datatypes.cons (existT _ _ ?v) ?ls
+ => let ls' := map_projT2 ls in
+ constr:(Datatypes.cons v ls')
+ end.
+
+ Ltac build_all_idents :=
+ let v := build_all_idents_gen (ident -> True) in
+ map_projT2 v.
+ Ltac make_all_idents := let v := build_all_idents in refine v.
+ End Tactics.
+
+ Definition all_idents : list ident := ltac:(make_all_idents).
+
+ Definition eta_ident_cps_gen {T : ident -> Type}
+ (f : forall idc, T idc)
+
+ : { f' : forall idc, T idc | forall idc, f' idc = f idc }.
+ Proof. make_eta_ident_cps_gen. Defined.
+
+ Definition eta_ident_cps_gen2
+ {T0 : ident -> Type}
+ (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.
+
+ Definition eta_ident_cps_gen3
+ {T0 : ident -> Type}
+ (f0 : forall idc, T0 idc)
+ {T1 : forall idc, T0 idc -> Type}
+ (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.
+
+ 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.
+ 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 ].
+ 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).
+
+ Inductive kind_of_type := GallinaType (_ : Type) | BaseBaseType | BaseType.
+ Definition Type_of_kind_of_type (T : kind_of_type)
+ := match T with
+ | GallinaType T => T
+ | BaseBaseType => Compilers.base.type.base
+ | BaseType => Compilers.base.type.type
end.
+ Notation type_of_list_of_kind ls
+ := (type_of_list (List.map Type_of_kind_of_type ls)).
+
+ Record preident_infos :=
+ {
+ dep_types : list Type; (* types which show up in the type of other infos *)
+ indep_types : list kind_of_type; (* types which show up in the type of the ident, but not in the type of other lists *)
+ indep_args : type_of_list dep_types -> list Type;
+ to_type : forall d : type_of_list dep_types, type_of_list_of_kind indep_types -> Compilers.type Compilers.base.type;
+ to_ident : forall (d : type_of_list dep_types) (i : type_of_list_of_kind indep_types), type_of_list (indep_args d) -> Compilers.ident.ident (to_type d i)
+ }.
+
+ Record ident_infos :=
+ {
+ preinfos :> preident_infos;
+ 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)
+ }.
+
+ Definition ident_args (pi : preident_infos)
+ := { t : type_of_list (dep_types pi) & type_of_list_of_kind (indep_types pi) * type_of_list (indep_args pi t) }%type.
+
+ 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).
+
+ Ltac fun_to_curried_ident_infos f :=
+ let type_to_kind T
+ := lazymatch (eval cbv beta in T) with
+ | Compilers.base.type.base => BaseBaseType
+ | Compilers.base.type.type => BaseType
+ | ?T => constr:(GallinaType T)
+ end in
+ let T := type of f in
+ lazymatch (eval cbv beta in T) with
+ | forall (x : ?A), _
+ => let f' := fresh in
+ let f := (eval cbv beta in
+ (fun x : A
+ => match f x return _ with
+ | f'
+ => ltac:(let f := (eval cbv [f'] in f') in
+ let res := fun_to_curried_ident_infos f in
+ exact res)
+ end)) in
+ let v
+ := match f with
+ | (fun x : ?A => {| dep_types := Datatypes.nil ; indep_types := Datatypes.nil ; indep_args := ?ida ; to_type := ?tt ; to_ident := @?ti x |})
+ => let d := fresh "d" in
+ let i := fresh "i" in
+ let a := fresh "a" in
+ constr:({| dep_types := Datatypes.nil ; indep_types := Datatypes.nil ; indep_args := (fun d => (A:Type) :: ida d) ; to_type := tt ; to_ident := fun d i a => ti (Datatypes.fst a) d i (Datatypes.snd a) |})
+ | (fun x : ?A => {| dep_types := Datatypes.nil ; indep_types := ?idt ; indep_args := ?ida ; to_type := @?tt x ; to_ident := @?ti x |})
+ => let d := fresh "d" in
+ let i := fresh "i" in
+ let a := fresh "a" in
+ let A := type_to_kind A in
+ constr:({| dep_types := Datatypes.nil ; indep_types := A :: idt ; indep_args := ida ; to_type := (fun d i => tt (Datatypes.fst i) d (Datatypes.snd i)) ; to_ident := fun d i a => ti (Datatypes.fst i) d (Datatypes.snd i) a |})
+ | (fun x : ?A => {| dep_types := ?dt ; indep_types := ?idt ; indep_args := @?ida x ; to_type := @?tt x ; to_ident := @?ti x |})
+ => let d := fresh "d" in
+ let i := fresh "i" in
+ let a := fresh "a" in
+ (*let A := type_to_kind A in*)
+ constr:({| dep_types := (A:Type) :: dt ; indep_types := idt ; indep_args := (fun d => ida (Datatypes.fst d) (Datatypes.snd d)) ; to_type := (fun d i => tt (Datatypes.fst d) (Datatypes.snd d) i) ; to_ident := fun d i a => ti (Datatypes.fst d) (Datatypes.snd d) i a |})
+ end in
+ (eval cbv beta in v)
+ | Compilers.ident.ident ?t
+ => constr:({| dep_types := Datatypes.nil ; indep_types := Datatypes.nil ; indep_args := (fun _ => Datatypes.nil) ; to_type := (fun _ _ => t) ; to_ident := fun _ _ _ => f |})
+ end.
+
+ Ltac build_ident_infos_of :=
+ let idc := fresh "idc" in
+ let T := fresh in
+ let v
+ := constr:(
+ fun idc : ident
+ => match ident_to_cident idc return ident_infos with
+ | T
+ => ltac:(destruct idc;
+ let T := (eval cbv [T ident_to_cident projT2] in (projT2 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) _ _ _);
+ 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
+ v.
+ Ltac make_ident_infos_of := let v := build_ident_infos_of in refine v.
+
+ Definition ident_infos_of : ident -> ident_infos := ltac:(make_ident_infos_of).
+
+ Ltac refine_sigT_and_pair :=
+ repeat first [ exact Datatypes.tt
+ | progress cbn [Datatypes.fst Datatypes.snd projT1 projT2]
+ | match goal with
+ | [ |- context[Datatypes.fst ?ev] ]
+ => is_evar ev;
+ let __ := open_constr:(eq_refl : ev = (_, _)) in
+ cbn [Datatypes.fst Datatypes.snd]
+ | [ |- context[Datatypes.snd ?ev] ]
+ => is_evar ev;
+ let __ := open_constr:(eq_refl : ev = (_, _)) in
+ cbn [Datatypes.fst Datatypes.snd]
+ | [ |- context[projT1 ?ev] ]
+ => is_evar ev;
+ let __ := open_constr:(eq_refl : ev = existT _ _ _) in
+ cbn [projT1 projT2]
+ | [ |- context[projT2 ?ev] ]
+ => is_evar ev;
+ let __ := open_constr:(eq_refl : ev = existT _ _ _) in
+ cbn [projT1 projT2]
+ end ].
+
+ Ltac build_split_ident_gen :=
+ let t := fresh "t" in
+ let idc := fresh "idc" in
+ let idc' := fresh "idc'" in
+ let ridc := fresh "ridc" in
+ let v := (eval cbv beta iota zeta in
+ (fun t (idc : Compilers.ident.ident t)
+ => let idc' := idc in
+ ltac:(destruct idc;
+ let idc := (eval cbv [idc'] in idc') in
+ let ctor := head idc in
+ let all_idents := (eval cbv [all_idents] in all_idents) in
+ let all_tidents := (eval cbv [pattern.all_idents] in pattern.all_idents) in
+ let ridc := find_ctor ctor all_tidents all_idents in
+ (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)
+ : { ridc : ident & { args : ident_args (ident_infos_of ridc)
+ | JMeq idc (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) } }
+ := 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 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).
+ 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 with
+ | [], [] => true
+ | _, _ => false
+ end))) in
+ refine v).
+ 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).
+ 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
+ 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).
End ident.
Notation ident := ident.ident.
End Raw.
Module ident.
+ Local Unset Decidable Equality Schemes.
+
Definition eta_ident_cps {T : Compilers.type Compilers.base.type -> Type} {t} (idc : Compilers.ident.ident t)
(f : forall t', Compilers.ident.ident t' -> T t')
: T t
- := match idc with
- | Compilers.ident.Literal t v => f _ (@Compilers.ident.Literal t v)
- | Compilers.ident.Nat_succ => f _ Compilers.ident.Nat_succ
- | Compilers.ident.Nat_pred => f _ Compilers.ident.Nat_pred
- | Compilers.ident.Nat_max => f _ Compilers.ident.Nat_max
- | Compilers.ident.Nat_mul => f _ Compilers.ident.Nat_mul
- | Compilers.ident.Nat_add => f _ Compilers.ident.Nat_add
- | Compilers.ident.Nat_sub => f _ Compilers.ident.Nat_sub
- | Compilers.ident.Nat_eqb => f _ Compilers.ident.Nat_eqb
- | Compilers.ident.nil t => f _ (@Compilers.ident.nil t)
- | Compilers.ident.cons t => f _ (@Compilers.ident.cons t)
- | Compilers.ident.pair A B => f _ (@Compilers.ident.pair A B)
- | Compilers.ident.fst A B => f _ (@Compilers.ident.fst A B)
- | Compilers.ident.snd A B => f _ (@Compilers.ident.snd A B)
- | Compilers.ident.prod_rect A B T => f _ (@Compilers.ident.prod_rect A B T)
- | Compilers.ident.bool_rect T => f _ (@Compilers.ident.bool_rect T)
- | Compilers.ident.nat_rect P => f _ (@Compilers.ident.nat_rect P)
- | Compilers.ident.nat_rect_arrow P Q => f _ (@Compilers.ident.nat_rect_arrow P Q)
- | 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)
- | Compilers.ident.List_length T => f _ (@Compilers.ident.List_length T)
- | Compilers.ident.List_seq => f _ Compilers.ident.List_seq
- | Compilers.ident.List_firstn A => f _ (@Compilers.ident.List_firstn A)
- | Compilers.ident.List_skipn A => f _ (@Compilers.ident.List_skipn A)
- | Compilers.ident.List_repeat A => f _ (@Compilers.ident.List_repeat A)
- | Compilers.ident.List_combine A B => f _ (@Compilers.ident.List_combine A B)
- | Compilers.ident.List_map A B => f _ (@Compilers.ident.List_map A B)
- | Compilers.ident.List_app A => f _ (@Compilers.ident.List_app A)
- | Compilers.ident.List_rev A => f _ (@Compilers.ident.List_rev A)
- | Compilers.ident.List_flat_map A B => f _ (@Compilers.ident.List_flat_map A B)
- | Compilers.ident.List_partition A => f _ (@Compilers.ident.List_partition A)
- | Compilers.ident.List_fold_right A B => f _ (@Compilers.ident.List_fold_right A B)
- | Compilers.ident.List_update_nth T => f _ (@Compilers.ident.List_update_nth T)
- | Compilers.ident.List_nth_default T => f _ (@Compilers.ident.List_nth_default T)
- | Compilers.ident.eager_List_nth_default T => f _ (@Compilers.ident.eager_List_nth_default T)
- | Compilers.ident.Z_add => f _ Compilers.ident.Z_add
- | Compilers.ident.Z_mul => f _ Compilers.ident.Z_mul
- | Compilers.ident.Z_pow => f _ Compilers.ident.Z_pow
- | Compilers.ident.Z_sub => f _ Compilers.ident.Z_sub
- | Compilers.ident.Z_opp => f _ Compilers.ident.Z_opp
- | Compilers.ident.Z_div => f _ Compilers.ident.Z_div
- | Compilers.ident.Z_modulo => f _ Compilers.ident.Z_modulo
- | Compilers.ident.Z_log2 => f _ Compilers.ident.Z_log2
- | Compilers.ident.Z_log2_up => f _ Compilers.ident.Z_log2_up
- | Compilers.ident.Z_eqb => f _ Compilers.ident.Z_eqb
- | Compilers.ident.Z_leb => f _ Compilers.ident.Z_leb
- | Compilers.ident.Z_ltb => f _ Compilers.ident.Z_ltb
- | Compilers.ident.Z_geb => f _ Compilers.ident.Z_geb
- | Compilers.ident.Z_gtb => f _ Compilers.ident.Z_gtb
- | Compilers.ident.Z_of_nat => f _ Compilers.ident.Z_of_nat
- | Compilers.ident.Z_to_nat => f _ Compilers.ident.Z_to_nat
- | Compilers.ident.Z_shiftr => f _ Compilers.ident.Z_shiftr
- | Compilers.ident.Z_shiftl => f _ Compilers.ident.Z_shiftl
- | Compilers.ident.Z_land => f _ Compilers.ident.Z_land
- | Compilers.ident.Z_lor => f _ Compilers.ident.Z_lor
- | Compilers.ident.Z_min => f _ Compilers.ident.Z_min
- | Compilers.ident.Z_max => f _ Compilers.ident.Z_max
- | Compilers.ident.Z_bneg => f _ Compilers.ident.Z_bneg
- | Compilers.ident.Z_lnot_modulo => f _ Compilers.ident.Z_lnot_modulo
- | Compilers.ident.Z_mul_split => f _ Compilers.ident.Z_mul_split
- | Compilers.ident.Z_add_get_carry => f _ Compilers.ident.Z_add_get_carry
- | Compilers.ident.Z_add_with_carry => f _ Compilers.ident.Z_add_with_carry
- | Compilers.ident.Z_add_with_get_carry => f _ Compilers.ident.Z_add_with_get_carry
- | Compilers.ident.Z_sub_get_borrow => f _ Compilers.ident.Z_sub_get_borrow
- | Compilers.ident.Z_sub_with_get_borrow => f _ Compilers.ident.Z_sub_with_get_borrow
- | Compilers.ident.Z_zselect => f _ Compilers.ident.Z_zselect
- | Compilers.ident.Z_add_modulo => f _ Compilers.ident.Z_add_modulo
- | Compilers.ident.Z_rshi => f _ Compilers.ident.Z_rshi
- | Compilers.ident.Z_cc_m => f _ Compilers.ident.Z_cc_m
- | Compilers.ident.Z_combine_at_bitwidth => f _ Compilers.ident.Z_combine_at_bitwidth
- | Compilers.ident.Z_cast range => f _ (@Compilers.ident.Z_cast range)
- | Compilers.ident.Z_cast2 range => f _ (@Compilers.ident.Z_cast2 range)
- | Compilers.ident.option_Some A => f _ (@Compilers.ident.option_Some A)
- | Compilers.ident.option_None A => f _ (@Compilers.ident.option_None A)
- | Compilers.ident.option_rect A P => f _ (@Compilers.ident.option_rect A P)
- | Compilers.ident.Build_zrange => f _ Compilers.ident.Build_zrange
- | Compilers.ident.zrange_rect P => f _ (@Compilers.ident.zrange_rect P)
- | Compilers.ident.fancy_add log2wordmax imm => f _ (@Compilers.ident.fancy_add log2wordmax imm)
- | Compilers.ident.fancy_addc log2wordmax imm => f _ (@Compilers.ident.fancy_addc log2wordmax imm)
- | Compilers.ident.fancy_sub log2wordmax imm => f _ (@Compilers.ident.fancy_sub log2wordmax imm)
- | Compilers.ident.fancy_subb log2wordmax imm => f _ (@Compilers.ident.fancy_subb log2wordmax imm)
- | Compilers.ident.fancy_mulll log2wordmax => f _ (@Compilers.ident.fancy_mulll log2wordmax)
- | Compilers.ident.fancy_mullh log2wordmax => f _ (@Compilers.ident.fancy_mullh log2wordmax)
- | Compilers.ident.fancy_mulhl log2wordmax => f _ (@Compilers.ident.fancy_mulhl log2wordmax)
- | Compilers.ident.fancy_mulhh log2wordmax => f _ (@Compilers.ident.fancy_mulhh log2wordmax)
- | Compilers.ident.fancy_rshi log2wordmax x => f _ (@Compilers.ident.fancy_rshi log2wordmax x)
- | Compilers.ident.fancy_selc => f _ Compilers.ident.fancy_selc
- | Compilers.ident.fancy_selm log2wordmax => f _ (@Compilers.ident.fancy_selm log2wordmax)
- | Compilers.ident.fancy_sell => f _ Compilers.ident.fancy_sell
- | Compilers.ident.fancy_addm => f _ Compilers.ident.fancy_addm
- end.
-
+ := Eval cbv [eta_ident_cps_gen proj1_sig] in
+ proj1_sig (@eta_ident_cps_gen (fun t _ => T t) f) t idc.
+
+ Module PrintIdent.
+ Import Compilers.ident.
+ Ltac map_projT2 tac ls :=
+ lazymatch ls with
+ | Datatypes.nil => idtac
+ | Datatypes.cons (existT _ _ ?v) ?ls
+ => tac v; map_projT2 tac ls
+ end.
+ Ltac fill_forall_args v :=
+ let T := type of v in
+ lazymatch (eval cbv beta in T) with
+ | ?A -> ?B => v
+ | forall x : ?A, _ => fill_forall_args open_constr:(v _)
+ | _ => v
+ end.
+ Ltac strip_nondep T :=
+ lazymatch T with
+ | ?A -> ?B => strip_nondep B
+ | forall x : ?A, ?B
+ => let B' := fresh in
+ constr:(forall x : A,
+ match B return _ with
+ | B' => ltac:(let B := (eval cbv [B'] in B') in
+ clear B';
+ let B := strip_nondep B in
+ exact B)
+ end)
+ | ?T => T
+ end.
+ Ltac print_ident :=
+ epose proof (_ : type -> Set) as ident;
+ idtac " Inductive ident : type -> Set :=";
+ let v := (eval cbv [pattern.all_idents Compilers.base.interp] in pattern.all_idents) in
+ map_projT2 ltac:(fun v
+ => let T := type of v in
+ let T := (eval cbv [Compilers.base.interp] in T) in
+ let T := strip_nondep T in
+ let T := (eval pattern Compilers.base.type.type, Compilers.base.type.prod, Compilers.base.type.list, Compilers.base.type.option, (@Compilers.base.type.type_base), (@Compilers.ident) in T) in
+ let T := lazymatch T with
+ | ?f _ _ _ _ _ _ => f
+ end in
+ let T := (eval cbv beta in
+ (T base.type.type base.type.prod base.type.list base.type.option (@base.type.type_base) (@ident))) in
+ let v := fill_forall_args v in
+ idtac " |" v ":" T) v;
+ idtac " .".
+ Local Set Printing Coercions.
+ Local Unset Printing Notations.
+ Local Set Printing Width 10000.
+ (*Goal True. print_ident. Abort.*)
+ End PrintIdent.
Inductive ident : type -> Set :=
- | Literal {t : base.type.base} : ident (type.base (base.type.type_base t))
- | Nat_succ : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat))%ptype
- | Nat_pred : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat))%ptype
- | Nat_max : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat))%ptype
- | Nat_mul : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat))%ptype
- | Nat_add : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat))%ptype
- | Nat_sub : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat))%ptype
- | Nat_eqb : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.bool))%ptype
- | nil {t : base.type} : ident (type.base (base.type.list t))
- | cons {t : base.type} : ident (type.base t -> type.base (base.type.list t) -> type.base (base.type.list t))%ptype
- | pair {A : base.type} {B : base.type} : ident (type.base A -> type.base B -> type.base (A * B)%pbtype)%ptype
- | fst {A : base.type} {B : base.type} : ident (type.base (A * B)%pbtype -> type.base A)%ptype
- | snd {A : base.type} {B : base.type} : ident (type.base (A * B)%pbtype -> type.base B)%ptype
- | prod_rect {A : base.type} {B : base.type} {T : base.type} : ident ((type.base A -> type.base B -> type.base T) -> type.base (A * B)%pbtype -> type.base T)%ptype
- | bool_rect {T : base.type} : ident ((type.base ()%pbtype -> type.base T) -> (type.base ()%pbtype -> type.base T) -> type.base (base.type.type_base base.type.bool) -> type.base T)%ptype
- | 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
- | 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
- | 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
- | List_length {T : base.type} : ident (type.base (base.type.list T) -> type.base (base.type.type_base base.type.nat))%ptype
- | List_seq : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.list (base.type.type_base base.type.nat)))%ptype
- | List_firstn {A : base.type} : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.list A) -> type.base (base.type.list A))%ptype
- | List_skipn {A : base.type} : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.list A) -> type.base (base.type.list A))%ptype
- | List_repeat {A : base.type} : ident (type.base A -> type.base (base.type.type_base base.type.nat) -> type.base (base.type.list A))%ptype
- | List_combine {A : base.type} {B : base.type} : ident (type.base (base.type.list A) -> type.base (base.type.list B) -> type.base (base.type.list (A * B)))%ptype
- | List_map {A : base.type} {B : base.type} : ident ((type.base A -> type.base B) -> type.base (base.type.list A) -> type.base (base.type.list B))%ptype
- | List_app {A : base.type} : ident (type.base (base.type.list A) -> type.base (base.type.list A) -> type.base (base.type.list A))%ptype
- | List_rev {A : base.type} : ident (type.base (base.type.list A) -> type.base (base.type.list A))%ptype
- | List_flat_map {A : base.type} {B : base.type} : ident ((type.base A -> type.base (base.type.list B)) -> type.base (base.type.list A) -> type.base (base.type.list B))%ptype
- | List_partition {A : base.type} : ident ((type.base A -> type.base (base.type.type_base base.type.bool)) -> type.base (base.type.list A) -> type.base (base.type.list A * base.type.list A)%pbtype)%ptype
- | List_fold_right {A : base.type} {B : base.type} : ident ((type.base B -> type.base A -> type.base A) -> type.base A -> type.base (base.type.list B) -> type.base A)%ptype
- | List_update_nth {T : base.type} : ident (type.base (base.type.type_base base.type.nat) -> (type.base T -> type.base T) -> type.base (base.type.list T) -> type.base (base.type.list T))%ptype
- | List_nth_default {T : base.type} : ident (type.base T -> type.base (base.type.list T) -> type.base (base.type.type_base base.type.nat) -> type.base T)%ptype
- | eager_List_nth_default {T : base.type} : ident (type.base T -> type.base (base.type.list T) -> type.base (base.type.type_base base.type.nat) -> type.base T)%ptype
- | Z_add : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_mul : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_pow : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_sub : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_opp : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_div : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_modulo : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_log2 : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_log2_up : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_eqb : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.bool))%ptype
- | Z_leb : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.bool))%ptype
- | Z_ltb : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.bool))%ptype
- | Z_geb : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.bool))%ptype
- | Z_gtb : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.bool))%ptype
- | Z_of_nat : ident (type.base (base.type.type_base base.type.nat) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_to_nat : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.nat))%ptype
- | Z_shiftr : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_shiftl : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_land : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_lor : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_min : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_max : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_bneg : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_lnot_modulo : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_mul_split : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
- | Z_add_get_carry : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
- | Z_add_with_carry : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_add_with_get_carry : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
- | Z_sub_get_borrow : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
- | Z_sub_with_get_borrow : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
- | Z_zselect : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_add_modulo : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_rshi : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_cc_m : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_combine_at_bitwidth : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_cast : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z))%ptype
- | Z_cast2 : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
- | option_Some {A : base.type} : ident (type.base A -> type.base (base.type.option A))%ptype
- | option_None {A : base.type} : ident (type.base (base.type.option A))
- | option_rect {A : base.type} {P : base.type} : ident ((type.base A -> type.base P) -> (type.base ()%pbtype -> type.base P) -> type.base (base.type.option A) -> type.base P)%ptype
- | Build_zrange : ident (type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.zrange))%ptype
- | zrange_rect {P : base.type} : ident ((type.base (base.type.type_base base.type.Z) -> type.base (base.type.type_base base.type.Z) -> type.base P) -> type.base (base.type.type_base base.type.zrange) -> type.base P)%ptype
- | fancy_add : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
- | fancy_addc : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
- | fancy_sub : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
- | fancy_subb : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype)%ptype
- | fancy_mulll : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
- | fancy_mullh : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
- | fancy_mulhl : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
- | fancy_mulhh : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
- | fancy_rshi : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
- | fancy_selc : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
- | fancy_selm : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
- | fancy_sell : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype
- | fancy_addm : ident (type.base (base.type.type_base base.type.Z * base.type.type_base base.type.Z * base.type.type_base base.type.Z)%pbtype -> type.base (base.type.type_base base.type.Z))%ptype.
-
- Definition strip_types {t} (idc : ident t) : Raw.ident
- := match idc with
- | @Literal t => Raw.ident.Literal
- | @Nat_succ => Raw.ident.Nat_succ
- | @Nat_pred => Raw.ident.Nat_pred
- | @Nat_max => Raw.ident.Nat_max
- | @Nat_mul => Raw.ident.Nat_mul
- | @Nat_add => Raw.ident.Nat_add
- | @Nat_sub => Raw.ident.Nat_sub
- | @Nat_eqb => Raw.ident.Nat_eqb
- | @nil t => Raw.ident.nil
- | @cons t => Raw.ident.cons
- | @pair A B => Raw.ident.pair
- | @fst A B => Raw.ident.fst
- | @snd A B => Raw.ident.snd
- | @prod_rect A B T => Raw.ident.prod_rect
- | @bool_rect T => Raw.ident.bool_rect
- | @nat_rect P => Raw.ident.nat_rect
- | @nat_rect_arrow P Q => Raw.ident.nat_rect_arrow
- | @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
- | @List_length T => Raw.ident.List_length
- | @List_seq => Raw.ident.List_seq
- | @List_firstn A => Raw.ident.List_firstn
- | @List_skipn A => Raw.ident.List_skipn
- | @List_repeat A => Raw.ident.List_repeat
- | @List_combine A B => Raw.ident.List_combine
- | @List_map A B => Raw.ident.List_map
- | @List_app A => Raw.ident.List_app
- | @List_rev A => Raw.ident.List_rev
- | @List_flat_map A B => Raw.ident.List_flat_map
- | @List_partition A => Raw.ident.List_partition
- | @List_fold_right A B => Raw.ident.List_fold_right
- | @List_update_nth T => Raw.ident.List_update_nth
- | @List_nth_default T => Raw.ident.List_nth_default
- | @eager_List_nth_default T => Raw.ident.eager_List_nth_default
- | @Z_add => Raw.ident.Z_add
- | @Z_mul => Raw.ident.Z_mul
- | @Z_pow => Raw.ident.Z_pow
- | @Z_sub => Raw.ident.Z_sub
- | @Z_opp => Raw.ident.Z_opp
- | @Z_div => Raw.ident.Z_div
- | @Z_modulo => Raw.ident.Z_modulo
- | @Z_log2 => Raw.ident.Z_log2
- | @Z_log2_up => Raw.ident.Z_log2_up
- | @Z_eqb => Raw.ident.Z_eqb
- | @Z_leb => Raw.ident.Z_leb
- | @Z_ltb => Raw.ident.Z_ltb
- | @Z_geb => Raw.ident.Z_geb
- | @Z_gtb => Raw.ident.Z_gtb
- | @Z_of_nat => Raw.ident.Z_of_nat
- | @Z_to_nat => Raw.ident.Z_to_nat
- | @Z_shiftr => Raw.ident.Z_shiftr
- | @Z_shiftl => Raw.ident.Z_shiftl
- | @Z_land => Raw.ident.Z_land
- | @Z_lor => Raw.ident.Z_lor
- | @Z_min => Raw.ident.Z_min
- | @Z_max => Raw.ident.Z_max
- | @Z_bneg => Raw.ident.Z_bneg
- | @Z_lnot_modulo => Raw.ident.Z_lnot_modulo
- | @Z_mul_split => Raw.ident.Z_mul_split
- | @Z_add_get_carry => Raw.ident.Z_add_get_carry
- | @Z_add_with_carry => Raw.ident.Z_add_with_carry
- | @Z_add_with_get_carry => Raw.ident.Z_add_with_get_carry
- | @Z_sub_get_borrow => Raw.ident.Z_sub_get_borrow
- | @Z_sub_with_get_borrow => Raw.ident.Z_sub_with_get_borrow
- | @Z_zselect => Raw.ident.Z_zselect
- | @Z_add_modulo => Raw.ident.Z_add_modulo
- | @Z_rshi => Raw.ident.Z_rshi
- | @Z_cc_m => Raw.ident.Z_cc_m
- | @Z_combine_at_bitwidth => Raw.ident.Z_combine_at_bitwidth
- | @Z_cast => Raw.ident.Z_cast
- | @Z_cast2 => Raw.ident.Z_cast2
- | @option_Some A => Raw.ident.option_Some
- | @option_None A => Raw.ident.option_None
- | @option_rect A P => Raw.ident.option_rect
- | @Build_zrange => Raw.ident.Build_zrange
- | @zrange_rect P => Raw.ident.zrange_rect
- | @fancy_add => Raw.ident.fancy_add
- | @fancy_addc => Raw.ident.fancy_addc
- | @fancy_sub => Raw.ident.fancy_sub
- | @fancy_subb => Raw.ident.fancy_subb
- | @fancy_mulll => Raw.ident.fancy_mulll
- | @fancy_mullh => Raw.ident.fancy_mullh
- | @fancy_mulhl => Raw.ident.fancy_mulhl
- | @fancy_mulhh => Raw.ident.fancy_mulhh
- | @fancy_rshi => Raw.ident.fancy_rshi
- | @fancy_selc => Raw.ident.fancy_selc
- | @fancy_selm => Raw.ident.fancy_selm
- | @fancy_sell => Raw.ident.fancy_sell
- | @fancy_addm => Raw.ident.fancy_addm
+ | Literal : (forall t : base.type.base, ident (type.base (base.type.type_base t)))
+ | Nat_succ : (ident (type.arrow (type.base (base.type.type_base base.type.nat)) (type.base (base.type.type_base base.type.nat))))
+ | Nat_pred : (ident (type.arrow (type.base (base.type.type_base base.type.nat)) (type.base (base.type.type_base base.type.nat))))
+ | Nat_max : (ident (type.arrow (type.base (base.type.type_base base.type.nat)) (type.arrow (type.base (base.type.type_base base.type.nat)) (type.base (base.type.type_base base.type.nat)))))
+ | Nat_mul : (ident (type.arrow (type.base (base.type.type_base base.type.nat)) (type.arrow (type.base (base.type.type_base base.type.nat)) (type.base (base.type.type_base base.type.nat)))))
+ | Nat_add : (ident (type.arrow (type.base (base.type.type_base base.type.nat)) (type.arrow (type.base (base.type.type_base base.type.nat)) (type.base (base.type.type_base base.type.nat)))))
+ | Nat_sub : (ident (type.arrow (type.base (base.type.type_base base.type.nat)) (type.arrow (type.base (base.type.type_base base.type.nat)) (type.base (base.type.type_base base.type.nat)))))
+ | Nat_eqb : (ident (type.arrow (type.base (base.type.type_base base.type.nat)) (type.arrow (type.base (base.type.type_base base.type.nat)) (type.base (base.type.type_base base.type.bool)))))
+ | nil : (forall t : base.type.type, ident (type.base (base.type.list t)))
+ | cons : (forall t : base.type.type, ident (type.arrow (type.base t) (type.arrow (type.base (base.type.list t)) (type.base (base.type.list t)))))
+ | pair : (forall A B : base.type.type, ident (type.arrow (type.base A) (type.arrow (type.base B) (type.base (base.type.prod A B)))))
+ | fst : (forall A B : base.type.type, ident (type.arrow (type.base (base.type.prod A B)) (type.base A)))
+ | snd : (forall A B : base.type.type, ident (type.arrow (type.base (base.type.prod A B)) (type.base B)))
+ | prod_rect : (forall A B T : base.type.type, ident (type.arrow (type.arrow (type.base A) (type.arrow (type.base B) (type.base T))) (type.arrow (type.base (base.type.prod A B)) (type.base T))))
+ | bool_rect : (forall T : base.type.type, ident (type.arrow (type.arrow (type.base (base.type.type_base base.type.unit)) (type.base T)) (type.arrow (type.arrow (type.base (base.type.type_base base.type.unit)) (type.base T)) (type.arrow (type.base (base.type.type_base base.type.bool)) (type.base T)))))
+ | nat_rect : (forall P : base.type.type, ident (type.arrow (type.arrow (type.base (base.type.type_base base.type.unit)) (type.base P)) (type.arrow (type.arrow (type.base (base.type.type_base base.type.nat)) (type.arrow (type.base P) (type.base P))) (type.arrow (type.base (base.type.type_base base.type.nat)) (type.base P)))))
+ | nat_rect_arrow : (forall P Q : base.type.type, ident (type.arrow (type.arrow (type.base P) (type.base Q)) (type.arrow (type.arrow (type.base (base.type.type_base base.type.nat)) (type.arrow (type.arrow (type.base P) (type.base Q)) (type.arrow (type.base P) (type.base Q)))) (type.arrow (type.base (base.type.type_base base.type.nat)) (type.arrow (type.base P) (type.base Q))))))
+ | eager_nat_rect : (forall P : base.type.type, ident (type.arrow (type.arrow (type.base (base.type.type_base base.type.unit)) (type.base P)) (type.arrow (type.arrow (type.base (base.type.type_base base.type.nat)) (type.arrow (type.base P) (type.base P))) (type.arrow (type.base (base.type.type_base base.type.nat)) (type.base P)))))
+ | eager_nat_rect_arrow : (forall P Q : base.type.type, ident (type.arrow (type.arrow (type.base P) (type.base Q)) (type.arrow (type.arrow (type.base (base.type.type_base base.type.nat)) (type.arrow (type.arrow (type.base P) (type.base Q)) (type.arrow (type.base P) (type.base Q)))) (type.arrow (type.base (base.type.type_base base.type.nat)) (type.arrow (type.base P) (type.base Q))))))
+ | list_rect : (forall A P : base.type.type, ident (type.arrow (type.arrow (type.base (base.type.type_base base.type.unit)) (type.base P)) (type.arrow (type.arrow (type.base A) (type.arrow (type.base (base.type.list A)) (type.arrow (type.base P) (type.base P)))) (type.arrow (type.base (base.type.list A)) (type.base P)))))
+ | list_rect_arrow : (forall A P Q : base.type.type, ident (type.arrow (type.arrow (type.base P) (type.base Q)) (type.arrow (type.arrow (type.base A) (type.arrow (type.base (base.type.list A)) (type.arrow (type.arrow (type.base P) (type.base Q)) (type.arrow (type.base P) (type.base Q))))) (type.arrow (type.base (base.type.list A)) (type.arrow (type.base P) (type.base Q))))))
+ | eager_list_rect : (forall A P : base.type.type, ident (type.arrow (type.arrow (type.base (base.type.type_base base.type.unit)) (type.base P)) (type.arrow (type.arrow (type.base A) (type.arrow (type.base (base.type.list A)) (type.arrow (type.base P) (type.base P)))) (type.arrow (type.base (base.type.list A)) (type.base P)))))
+ | eager_list_rect_arrow : (forall A P Q : base.type.type, ident (type.arrow (type.arrow (type.base P) (type.base Q)) (type.arrow (type.arrow (type.base A) (type.arrow (type.base (base.type.list A)) (type.arrow (type.arrow (type.base P) (type.base Q)) (type.arrow (type.base P) (type.base Q))))) (type.arrow (type.base (base.type.list A)) (type.arrow (type.base P) (type.base Q))))))
+ | list_case : (forall A P : base.type.type, ident (type.arrow (type.arrow (type.base (base.type.type_base base.type.unit)) (type.base P)) (type.arrow (type.arrow (type.base A) (type.arrow (type.base (base.type.list A)) (type.base P))) (type.arrow (type.base (base.type.list A)) (type.base P)))))
+ | List_length : (forall T : base.type.type, ident (type.arrow (type.base (base.type.list T)) (type.base (base.type.type_base base.type.nat))))
+ | List_seq : (ident (type.arrow (type.base (base.type.type_base base.type.nat)) (type.arrow (type.base (base.type.type_base base.type.nat)) (type.base (base.type.list (base.type.type_base base.type.nat))))))
+ | List_firstn : (forall A : base.type.type, ident (type.arrow (type.base (base.type.type_base base.type.nat)) (type.arrow (type.base (base.type.list A)) (type.base (base.type.list A)))))
+ | List_skipn : (forall A : base.type.type, ident (type.arrow (type.base (base.type.type_base base.type.nat)) (type.arrow (type.base (base.type.list A)) (type.base (base.type.list A)))))
+ | List_repeat : (forall A : base.type.type, ident (type.arrow (type.base A) (type.arrow (type.base (base.type.type_base base.type.nat)) (type.base (base.type.list A)))))
+ | List_combine : (forall A B : base.type.type, ident (type.arrow (type.base (base.type.list A)) (type.arrow (type.base (base.type.list B)) (type.base (base.type.list (base.type.prod A B))))))
+ | List_map : (forall A B : base.type.type, ident (type.arrow (type.arrow (type.base A) (type.base B)) (type.arrow (type.base (base.type.list A)) (type.base (base.type.list B)))))
+ | List_app : (forall A : base.type.type, ident (type.arrow (type.base (base.type.list A)) (type.arrow (type.base (base.type.list A)) (type.base (base.type.list A)))))
+ | List_rev : (forall A : base.type.type, ident (type.arrow (type.base (base.type.list A)) (type.base (base.type.list A))))
+ | List_flat_map : (forall A B : base.type.type, ident (type.arrow (type.arrow (type.base A) (type.base (base.type.list B))) (type.arrow (type.base (base.type.list A)) (type.base (base.type.list B)))))
+ | List_partition : (forall A : base.type.type, ident (type.arrow (type.arrow (type.base A) (type.base (base.type.type_base base.type.bool))) (type.arrow (type.base (base.type.list A)) (type.base (base.type.prod (base.type.list A) (base.type.list A))))))
+ | List_fold_right : (forall A B : base.type.type, ident (type.arrow (type.arrow (type.base B) (type.arrow (type.base A) (type.base A))) (type.arrow (type.base A) (type.arrow (type.base (base.type.list B)) (type.base A)))))
+ | List_update_nth : (forall T : base.type.type, ident (type.arrow (type.base (base.type.type_base base.type.nat)) (type.arrow (type.arrow (type.base T) (type.base T)) (type.arrow (type.base (base.type.list T)) (type.base (base.type.list T))))))
+ | List_nth_default : (forall T : base.type.type, ident (type.arrow (type.base T) (type.arrow (type.base (base.type.list T)) (type.arrow (type.base (base.type.type_base base.type.nat)) (type.base T)))))
+ | eager_List_nth_default : (forall T : base.type.type, ident (type.arrow (type.base T) (type.arrow (type.base (base.type.list T)) (type.arrow (type.base (base.type.type_base base.type.nat)) (type.base T)))))
+ | Z_add : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z)))))
+ | Z_mul : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z)))))
+ | Z_pow : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z)))))
+ | Z_sub : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z)))))
+ | Z_opp : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z))))
+ | Z_div : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z)))))
+ | Z_modulo : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z)))))
+ | Z_log2 : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z))))
+ | Z_log2_up : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z))))
+ | Z_eqb : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.bool)))))
+ | Z_leb : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.bool)))))
+ | Z_ltb : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.bool)))))
+ | Z_geb : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.bool)))))
+ | Z_gtb : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.bool)))))
+ | Z_of_nat : (ident (type.arrow (type.base (base.type.type_base base.type.nat)) (type.base (base.type.type_base base.type.Z))))
+ | Z_to_nat : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.nat))))
+ | Z_shiftr : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z)))))
+ | Z_shiftl : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z)))))
+ | Z_land : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z)))))
+ | Z_lor : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z)))))
+ | Z_min : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z)))))
+ | Z_max : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z)))))
+ | Z_bneg : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z))))
+ | Z_lnot_modulo : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z)))))
+ | Z_mul_split : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)))))))
+ | Z_add_get_carry : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)))))))
+ | Z_add_with_carry : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z))))))
+ | Z_add_with_get_carry : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z))))))))
+ | Z_sub_get_borrow : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)))))))
+ | Z_sub_with_get_borrow : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z))))))))
+ | Z_zselect : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z))))))
+ | Z_add_modulo : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z))))))
+ | Z_rshi : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z)))))))
+ | Z_cc_m : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z)))))
+ | Z_combine_at_bitwidth : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z))))))
+ | Z_cast : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.Z))))
+ | Z_cast2 : (ident (type.arrow (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z))) (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)))))
+ | option_Some : (forall A : base.type.type, ident (type.arrow (type.base A) (type.base (base.type.option A))))
+ | option_None : (forall A : base.type.type, ident (type.base (base.type.option A)))
+ | option_rect : (forall A P : base.type.type, ident (type.arrow (type.arrow (type.base A) (type.base P)) (type.arrow (type.arrow (type.base (base.type.type_base base.type.unit)) (type.base P)) (type.arrow (type.base (base.type.option A)) (type.base P)))))
+ | Build_zrange : (ident (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base (base.type.type_base base.type.zrange)))))
+ | zrange_rect : (forall P : base.type.type, ident (type.arrow (type.arrow (type.base (base.type.type_base base.type.Z)) (type.arrow (type.base (base.type.type_base base.type.Z)) (type.base P))) (type.arrow (type.base (base.type.type_base base.type.zrange)) (type.base P))))
+ | fancy_add : (ident (type.arrow (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z))) (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)))))
+ | fancy_addc : (ident (type.arrow (type.base (base.type.prod (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)) (base.type.type_base base.type.Z))) (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)))))
+ | fancy_sub : (ident (type.arrow (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z))) (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)))))
+ | fancy_subb : (ident (type.arrow (type.base (base.type.prod (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)) (base.type.type_base base.type.Z))) (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)))))
+ | fancy_mulll : (ident (type.arrow (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z))) (type.base (base.type.type_base base.type.Z))))
+ | fancy_mullh : (ident (type.arrow (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z))) (type.base (base.type.type_base base.type.Z))))
+ | fancy_mulhl : (ident (type.arrow (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z))) (type.base (base.type.type_base base.type.Z))))
+ | fancy_mulhh : (ident (type.arrow (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z))) (type.base (base.type.type_base base.type.Z))))
+ | fancy_rshi : (ident (type.arrow (type.base (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z))) (type.base (base.type.type_base base.type.Z))))
+ | fancy_selc : (ident (type.arrow (type.base (base.type.prod (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)) (base.type.type_base base.type.Z))) (type.base (base.type.type_base base.type.Z))))
+ | fancy_selm : (ident (type.arrow (type.base (base.type.prod (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)) (base.type.type_base base.type.Z))) (type.base (base.type.type_base base.type.Z))))
+ | fancy_sell : (ident (type.arrow (type.base (base.type.prod (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)) (base.type.type_base base.type.Z))) (type.base (base.type.type_base base.type.Z))))
+ | fancy_addm : (ident (type.arrow (type.base (base.type.prod (base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z)) (base.type.type_base base.type.Z))) (type.base (base.type.type_base base.type.Z))))
+ .
+
+ Ltac build_all_idents := build_all_idents_gen (forall t (idc : ident t), True).
+ Ltac make_all_idents := let v := build_all_idents in refine v.
+
+ Definition all_idents : list { T : Type & T } := ltac:(make_all_idents).
+
+ Definition eta_ident_cps_gen
+ {T : forall t, ident t -> Type}
+ (f : forall t idc, T t idc)
+ : { f' : forall t idc, T t idc | forall t idc, f' t idc = f t idc }.
+ Proof. make_eta_ident_cps_gen. Defined.
+
+ Definition eta_ident_cps_gen_expand_literal
+ {T : forall t, ident t -> Type}
+ (f : forall t idc, T t idc)
+ : { f' : forall t idc, T t idc | forall t idc, f' t idc = f t idc }.
+ Proof. make_eta_ident_cps_gen_expand_literal. Defined.
+
+ Definition eta_ident_cps_gen2
+ {T0 : forall t, ident t -> Type}
+ (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.
+
+ 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}
+ (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.
+
+ Definition Type_of_kind_of_type (T : Raw.ident.kind_of_type)
+ := match T with
+ | Raw.ident.GallinaType T => T
+ | Raw.ident.BaseBaseType => Compilers.base.type.base
+ | Raw.ident.BaseType => pattern.base.type.type
end.
- Definition arg_types {t} (idc : ident t) : list Type
- := match idc return list Type with
- | @Literal t => [base.interp (Compilers.base.type.type_base t) : Type]
- | @Nat_succ => []
- | @Nat_pred => []
- | @Nat_max => []
- | @Nat_mul => []
- | @Nat_add => []
- | @Nat_sub => []
- | @Nat_eqb => []
- | @nil t => []
- | @cons t => []
- | @pair A B => []
- | @fst A B => []
- | @snd A B => []
- | @prod_rect A B T => []
- | @bool_rect T => []
- | @nat_rect P => []
- | @nat_rect_arrow P Q => []
- | @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 => []
- | @List_length T => []
- | @List_seq => []
- | @List_firstn A => []
- | @List_skipn A => []
- | @List_repeat A => []
- | @List_combine A B => []
- | @List_map A B => []
- | @List_app A => []
- | @List_rev A => []
- | @List_flat_map A B => []
- | @List_partition A => []
- | @List_fold_right A B => []
- | @List_update_nth T => []
- | @List_nth_default T => []
- | @eager_List_nth_default T => []
- | @Z_add => []
- | @Z_mul => []
- | @Z_pow => []
- | @Z_sub => []
- | @Z_opp => []
- | @Z_div => []
- | @Z_modulo => []
- | @Z_log2 => []
- | @Z_log2_up => []
- | @Z_eqb => []
- | @Z_leb => []
- | @Z_ltb => []
- | @Z_geb => []
- | @Z_gtb => []
- | @Z_of_nat => []
- | @Z_to_nat => []
- | @Z_shiftr => []
- | @Z_shiftl => []
- | @Z_land => []
- | @Z_lor => []
- | @Z_min => []
- | @Z_max => []
- | @Z_bneg => []
- | @Z_lnot_modulo => []
- | @Z_mul_split => []
- | @Z_add_get_carry => []
- | @Z_add_with_carry => []
- | @Z_add_with_get_carry => []
- | @Z_sub_get_borrow => []
- | @Z_sub_with_get_borrow => []
- | @Z_zselect => []
- | @Z_add_modulo => []
- | @Z_rshi => []
- | @Z_cc_m => []
- | @Z_combine_at_bitwidth => []
- | @Z_cast => [zrange : Type]
- | @Z_cast2 => [zrange * zrange : Type]
- | @option_Some A => []
- | @option_None A => []
- | @option_rect A P => []
- | @Build_zrange => []
- | @zrange_rect P => []
- | @fancy_add => [Z : Type; Z : Type]
- | @fancy_addc => [Z : Type; Z : Type]
- | @fancy_sub => [Z : Type; Z : Type]
- | @fancy_subb => [Z : Type; Z : Type]
- | @fancy_mulll => [Z : Type]
- | @fancy_mullh => [Z : Type]
- | @fancy_mulhl => [Z : Type]
- | @fancy_mulhh => [Z : Type]
- | @fancy_rshi => [Z : Type; Z : Type]
- | @fancy_selc => []
- | @fancy_selm => [Z : Type]
- | @fancy_sell => []
- | @fancy_addm => []
- end%type.
-
- Definition to_typed {t} (idc : ident t) (evm : EvarMap) : type_of_list (arg_types idc) -> Compilers.ident.ident (pattern.type.subst_default t evm)
- := match idc in ident t return type_of_list (arg_types idc) -> Compilers.ident.ident (pattern.type.subst_default t evm) with
- | @Literal t => fun arg => let '(v, _) := eta2r arg in @Compilers.ident.Literal _ v
- | @Nat_succ => fun _ => @Compilers.ident.Nat_succ
- | @Nat_pred => fun _ => @Compilers.ident.Nat_pred
- | @Nat_max => fun _ => @Compilers.ident.Nat_max
- | @Nat_mul => fun _ => @Compilers.ident.Nat_mul
- | @Nat_add => fun _ => @Compilers.ident.Nat_add
- | @Nat_sub => fun _ => @Compilers.ident.Nat_sub
- | @Nat_eqb => fun _ => @Compilers.ident.Nat_eqb
- | @nil t => fun _ => @Compilers.ident.nil _
- | @cons t => fun _ => @Compilers.ident.cons _
- | @pair A B => fun _ => @Compilers.ident.pair _ _
- | @fst A B => fun _ => @Compilers.ident.fst _ _
- | @snd A B => fun _ => @Compilers.ident.snd _ _
- | @prod_rect A B T => fun _ => @Compilers.ident.prod_rect _ _ _
- | @bool_rect T => fun _ => @Compilers.ident.bool_rect _
- | @nat_rect P => fun _ => @Compilers.ident.nat_rect _
- | @nat_rect_arrow P Q => fun _ => @Compilers.ident.nat_rect_arrow _ _
- | @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 _ _
- | @List_length T => fun _ => @Compilers.ident.List_length _
- | @List_seq => fun _ => @Compilers.ident.List_seq
- | @List_firstn A => fun _ => @Compilers.ident.List_firstn _
- | @List_skipn A => fun _ => @Compilers.ident.List_skipn _
- | @List_repeat A => fun _ => @Compilers.ident.List_repeat _
- | @List_combine A B => fun _ => @Compilers.ident.List_combine _ _
- | @List_map A B => fun _ => @Compilers.ident.List_map _ _
- | @List_app A => fun _ => @Compilers.ident.List_app _
- | @List_rev A => fun _ => @Compilers.ident.List_rev _
- | @List_flat_map A B => fun _ => @Compilers.ident.List_flat_map _ _
- | @List_partition A => fun _ => @Compilers.ident.List_partition _
- | @List_fold_right A B => fun _ => @Compilers.ident.List_fold_right _ _
- | @List_update_nth T => fun _ => @Compilers.ident.List_update_nth _
- | @List_nth_default T => fun _ => @Compilers.ident.List_nth_default _
- | @eager_List_nth_default T => fun _ => @Compilers.ident.eager_List_nth_default _
- | @Z_add => fun _ => @Compilers.ident.Z_add
- | @Z_mul => fun _ => @Compilers.ident.Z_mul
- | @Z_pow => fun _ => @Compilers.ident.Z_pow
- | @Z_sub => fun _ => @Compilers.ident.Z_sub
- | @Z_opp => fun _ => @Compilers.ident.Z_opp
- | @Z_div => fun _ => @Compilers.ident.Z_div
- | @Z_modulo => fun _ => @Compilers.ident.Z_modulo
- | @Z_log2 => fun _ => @Compilers.ident.Z_log2
- | @Z_log2_up => fun _ => @Compilers.ident.Z_log2_up
- | @Z_eqb => fun _ => @Compilers.ident.Z_eqb
- | @Z_leb => fun _ => @Compilers.ident.Z_leb
- | @Z_ltb => fun _ => @Compilers.ident.Z_ltb
- | @Z_geb => fun _ => @Compilers.ident.Z_geb
- | @Z_gtb => fun _ => @Compilers.ident.Z_gtb
- | @Z_of_nat => fun _ => @Compilers.ident.Z_of_nat
- | @Z_to_nat => fun _ => @Compilers.ident.Z_to_nat
- | @Z_shiftr => fun _ => @Compilers.ident.Z_shiftr
- | @Z_shiftl => fun _ => @Compilers.ident.Z_shiftl
- | @Z_land => fun _ => @Compilers.ident.Z_land
- | @Z_lor => fun _ => @Compilers.ident.Z_lor
- | @Z_min => fun _ => @Compilers.ident.Z_min
- | @Z_max => fun _ => @Compilers.ident.Z_max
- | @Z_bneg => fun _ => @Compilers.ident.Z_bneg
- | @Z_lnot_modulo => fun _ => @Compilers.ident.Z_lnot_modulo
- | @Z_mul_split => fun _ => @Compilers.ident.Z_mul_split
- | @Z_add_get_carry => fun _ => @Compilers.ident.Z_add_get_carry
- | @Z_add_with_carry => fun _ => @Compilers.ident.Z_add_with_carry
- | @Z_add_with_get_carry => fun _ => @Compilers.ident.Z_add_with_get_carry
- | @Z_sub_get_borrow => fun _ => @Compilers.ident.Z_sub_get_borrow
- | @Z_sub_with_get_borrow => fun _ => @Compilers.ident.Z_sub_with_get_borrow
- | @Z_zselect => fun _ => @Compilers.ident.Z_zselect
- | @Z_add_modulo => fun _ => @Compilers.ident.Z_add_modulo
- | @Z_rshi => fun _ => @Compilers.ident.Z_rshi
- | @Z_cc_m => fun _ => @Compilers.ident.Z_cc_m
- | @Z_combine_at_bitwidth => fun _ => @Compilers.ident.Z_combine_at_bitwidth
- | @Z_cast => fun arg => let '(range, _) := eta2r arg in @Compilers.ident.Z_cast range
- | @Z_cast2 => fun arg => let '(range, _) := eta2r arg in @Compilers.ident.Z_cast2 range
- | @option_Some A => fun _ => @Compilers.ident.option_Some _
- | @option_None A => fun _ => @Compilers.ident.option_None _
- | @option_rect A P => fun _ => @Compilers.ident.option_rect _ _
- | @Build_zrange => fun _ => @Compilers.ident.Build_zrange
- | @zrange_rect P => fun _ => @Compilers.ident.zrange_rect _
- | @fancy_add => fun arg => let '(log2wordmax, (imm, _)) := eta3r arg in @Compilers.ident.fancy_add log2wordmax imm
- | @fancy_addc => fun arg => let '(log2wordmax, (imm, _)) := eta3r arg in @Compilers.ident.fancy_addc log2wordmax imm
- | @fancy_sub => fun arg => let '(log2wordmax, (imm, _)) := eta3r arg in @Compilers.ident.fancy_sub log2wordmax imm
- | @fancy_subb => fun arg => let '(log2wordmax, (imm, _)) := eta3r arg in @Compilers.ident.fancy_subb log2wordmax imm
- | @fancy_mulll => fun arg => let '(log2wordmax, _) := eta2r arg in @Compilers.ident.fancy_mulll log2wordmax
- | @fancy_mullh => fun arg => let '(log2wordmax, _) := eta2r arg in @Compilers.ident.fancy_mullh log2wordmax
- | @fancy_mulhl => fun arg => let '(log2wordmax, _) := eta2r arg in @Compilers.ident.fancy_mulhl log2wordmax
- | @fancy_mulhh => fun arg => let '(log2wordmax, _) := eta2r arg in @Compilers.ident.fancy_mulhh log2wordmax
- | @fancy_rshi => fun arg => let '(log2wordmax, (x, _)) := eta3r arg in @Compilers.ident.fancy_rshi log2wordmax x
- | @fancy_selc => fun _ => @Compilers.ident.fancy_selc
- | @fancy_selm => fun arg => let '(log2wordmax, _) := eta2r arg in @Compilers.ident.fancy_selm log2wordmax
- | @fancy_sell => fun _ => @Compilers.ident.fancy_sell
- | @fancy_addm => fun _ => @Compilers.ident.fancy_addm
- end.
+ Notation type_of_list_of_kind ls
+ := (type_of_list (List.map Type_of_kind_of_type ls)).
- Definition unify {t t'} (pidc : ident t) (idc : Compilers.ident.ident t') : Datatypes.option (type_of_list (@arg_types t pidc))
- := match pidc, idc return Datatypes.option (type_of_list (arg_types pidc)) with
- | @Literal Compilers.base.type.unit, Compilers.ident.Literal Compilers.base.type.unit v => Datatypes.Some (v, tt)
- | @Literal Compilers.base.type.Z, Compilers.ident.Literal Compilers.base.type.Z v => Datatypes.Some (v, tt)
- | @Literal Compilers.base.type.bool, Compilers.ident.Literal Compilers.base.type.bool v => Datatypes.Some (v, tt)
- | @Literal Compilers.base.type.nat, Compilers.ident.Literal Compilers.base.type.nat v => Datatypes.Some (v, tt)
- | @Literal Compilers.base.type.zrange, Compilers.ident.Literal Compilers.base.type.zrange v => Datatypes.Some (v, tt)
- | @Nat_succ, Compilers.ident.Nat_succ => Datatypes.Some tt
- | @Nat_pred, Compilers.ident.Nat_pred => Datatypes.Some tt
- | @Nat_max, Compilers.ident.Nat_max => Datatypes.Some tt
- | @Nat_mul, Compilers.ident.Nat_mul => Datatypes.Some tt
- | @Nat_add, Compilers.ident.Nat_add => Datatypes.Some tt
- | @Nat_sub, Compilers.ident.Nat_sub => Datatypes.Some tt
- | @Nat_eqb, Compilers.ident.Nat_eqb => Datatypes.Some tt
- | @nil t, Compilers.ident.nil t' => Datatypes.Some tt
- | @cons t, Compilers.ident.cons t' => Datatypes.Some tt
- | @pair A B, Compilers.ident.pair A' B' => Datatypes.Some tt
- | @fst A B, Compilers.ident.fst A' B' => Datatypes.Some tt
- | @snd A B, Compilers.ident.snd A' B' => Datatypes.Some tt
- | @prod_rect A B T, Compilers.ident.prod_rect A' B' T' => Datatypes.Some tt
- | @bool_rect T, Compilers.ident.bool_rect T' => Datatypes.Some tt
- | @nat_rect P, Compilers.ident.nat_rect P' => Datatypes.Some tt
- | @nat_rect_arrow P Q, Compilers.ident.nat_rect_arrow P' Q' => Datatypes.Some tt
- | @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
- | @List_length T, Compilers.ident.List_length T' => Datatypes.Some tt
- | @List_seq, Compilers.ident.List_seq => Datatypes.Some tt
- | @List_firstn A, Compilers.ident.List_firstn A' => Datatypes.Some tt
- | @List_skipn A, Compilers.ident.List_skipn A' => Datatypes.Some tt
- | @List_repeat A, Compilers.ident.List_repeat A' => Datatypes.Some tt
- | @List_combine A B, Compilers.ident.List_combine A' B' => Datatypes.Some tt
- | @List_map A B, Compilers.ident.List_map A' B' => Datatypes.Some tt
- | @List_app A, Compilers.ident.List_app A' => Datatypes.Some tt
- | @List_rev A, Compilers.ident.List_rev A' => Datatypes.Some tt
- | @List_flat_map A B, Compilers.ident.List_flat_map A' B' => Datatypes.Some tt
- | @List_partition A, Compilers.ident.List_partition A' => Datatypes.Some tt
- | @List_fold_right A B, Compilers.ident.List_fold_right A' B' => Datatypes.Some tt
- | @List_update_nth T, Compilers.ident.List_update_nth T' => Datatypes.Some tt
- | @List_nth_default T, Compilers.ident.List_nth_default T' => Datatypes.Some tt
- | @eager_List_nth_default T, Compilers.ident.eager_List_nth_default T' => Datatypes.Some tt
- | @Z_add, Compilers.ident.Z_add => Datatypes.Some tt
- | @Z_mul, Compilers.ident.Z_mul => Datatypes.Some tt
- | @Z_pow, Compilers.ident.Z_pow => Datatypes.Some tt
- | @Z_sub, Compilers.ident.Z_sub => Datatypes.Some tt
- | @Z_opp, Compilers.ident.Z_opp => Datatypes.Some tt
- | @Z_div, Compilers.ident.Z_div => Datatypes.Some tt
- | @Z_modulo, Compilers.ident.Z_modulo => Datatypes.Some tt
- | @Z_log2, Compilers.ident.Z_log2 => Datatypes.Some tt
- | @Z_log2_up, Compilers.ident.Z_log2_up => Datatypes.Some tt
- | @Z_eqb, Compilers.ident.Z_eqb => Datatypes.Some tt
- | @Z_leb, Compilers.ident.Z_leb => Datatypes.Some tt
- | @Z_ltb, Compilers.ident.Z_ltb => Datatypes.Some tt
- | @Z_geb, Compilers.ident.Z_geb => Datatypes.Some tt
- | @Z_gtb, Compilers.ident.Z_gtb => Datatypes.Some tt
- | @Z_of_nat, Compilers.ident.Z_of_nat => Datatypes.Some tt
- | @Z_to_nat, Compilers.ident.Z_to_nat => Datatypes.Some tt
- | @Z_shiftr, Compilers.ident.Z_shiftr => Datatypes.Some tt
- | @Z_shiftl, Compilers.ident.Z_shiftl => Datatypes.Some tt
- | @Z_land, Compilers.ident.Z_land => Datatypes.Some tt
- | @Z_lor, Compilers.ident.Z_lor => Datatypes.Some tt
- | @Z_min, Compilers.ident.Z_min => Datatypes.Some tt
- | @Z_max, Compilers.ident.Z_max => Datatypes.Some tt
- | @Z_bneg, Compilers.ident.Z_bneg => Datatypes.Some tt
- | @Z_lnot_modulo, Compilers.ident.Z_lnot_modulo => Datatypes.Some tt
- | @Z_mul_split, Compilers.ident.Z_mul_split => Datatypes.Some tt
- | @Z_add_get_carry, Compilers.ident.Z_add_get_carry => Datatypes.Some tt
- | @Z_add_with_carry, Compilers.ident.Z_add_with_carry => Datatypes.Some tt
- | @Z_add_with_get_carry, Compilers.ident.Z_add_with_get_carry => Datatypes.Some tt
- | @Z_sub_get_borrow, Compilers.ident.Z_sub_get_borrow => Datatypes.Some tt
- | @Z_sub_with_get_borrow, Compilers.ident.Z_sub_with_get_borrow => Datatypes.Some tt
- | @Z_zselect, Compilers.ident.Z_zselect => Datatypes.Some tt
- | @Z_add_modulo, Compilers.ident.Z_add_modulo => Datatypes.Some tt
- | @Z_rshi, Compilers.ident.Z_rshi => Datatypes.Some tt
- | @Z_cc_m, Compilers.ident.Z_cc_m => Datatypes.Some tt
- | @Z_combine_at_bitwidth, Compilers.ident.Z_combine_at_bitwidth => Datatypes.Some tt
- | @Z_cast, Compilers.ident.Z_cast range' => Datatypes.Some (range', tt)
- | @Z_cast2, Compilers.ident.Z_cast2 range' => Datatypes.Some (range', tt)
- | @option_Some A, Compilers.ident.option_Some A' => Datatypes.Some tt
- | @option_None A, Compilers.ident.option_None A' => Datatypes.Some tt
- | @option_rect A P, Compilers.ident.option_rect A' P' => Datatypes.Some tt
- | @Build_zrange, Compilers.ident.Build_zrange => Datatypes.Some tt
- | @zrange_rect P, Compilers.ident.zrange_rect P' => Datatypes.Some tt
- | @fancy_add, Compilers.ident.fancy_add log2wordmax' imm' => Datatypes.Some (log2wordmax', (imm', tt))
- | @fancy_addc, Compilers.ident.fancy_addc log2wordmax' imm' => Datatypes.Some (log2wordmax', (imm', tt))
- | @fancy_sub, Compilers.ident.fancy_sub log2wordmax' imm' => Datatypes.Some (log2wordmax', (imm', tt))
- | @fancy_subb, Compilers.ident.fancy_subb log2wordmax' imm' => Datatypes.Some (log2wordmax', (imm', tt))
- | @fancy_mulll, Compilers.ident.fancy_mulll log2wordmax' => Datatypes.Some (log2wordmax', tt)
- | @fancy_mullh, Compilers.ident.fancy_mullh log2wordmax' => Datatypes.Some (log2wordmax', tt)
- | @fancy_mulhl, Compilers.ident.fancy_mulhl log2wordmax' => Datatypes.Some (log2wordmax', tt)
- | @fancy_mulhh, Compilers.ident.fancy_mulhh log2wordmax' => Datatypes.Some (log2wordmax', tt)
- | @fancy_rshi, Compilers.ident.fancy_rshi log2wordmax' x' => Datatypes.Some (log2wordmax', (x', tt))
- | @fancy_selc, Compilers.ident.fancy_selc => Datatypes.Some tt
- | @fancy_selm, Compilers.ident.fancy_selm log2wordmax' => Datatypes.Some (log2wordmax', tt)
- | @fancy_sell, Compilers.ident.fancy_sell => Datatypes.Some tt
- | @fancy_addm, Compilers.ident.fancy_addm => Datatypes.Some tt
- | @Literal _, _
- | @Nat_succ, _
- | @Nat_pred, _
- | @Nat_max, _
- | @Nat_mul, _
- | @Nat_add, _
- | @Nat_sub, _
- | @Nat_eqb, _
- | @nil _, _
- | @cons _, _
- | @pair _ _, _
- | @fst _ _, _
- | @snd _ _, _
- | @prod_rect _ _ _, _
- | @bool_rect _, _
- | @nat_rect _, _
- | @nat_rect_arrow _ _, _
- | @eager_nat_rect _, _
- | @eager_nat_rect_arrow _ _, _
- | @list_rect _ _, _
- | @list_rect_arrow _ _ _, _
- | @eager_list_rect _ _, _
- | @eager_list_rect_arrow _ _ _, _
- | @list_case _ _, _
- | @List_length _, _
- | @List_seq, _
- | @List_firstn _, _
- | @List_skipn _, _
- | @List_repeat _, _
- | @List_combine _ _, _
- | @List_map _ _, _
- | @List_app _, _
- | @List_rev _, _
- | @List_flat_map _ _, _
- | @List_partition _, _
- | @List_fold_right _ _, _
- | @List_update_nth _, _
- | @List_nth_default _, _
- | @eager_List_nth_default _, _
- | @Z_add, _
- | @Z_mul, _
- | @Z_pow, _
- | @Z_sub, _
- | @Z_opp, _
- | @Z_div, _
- | @Z_modulo, _
- | @Z_log2, _
- | @Z_log2_up, _
- | @Z_eqb, _
- | @Z_leb, _
- | @Z_ltb, _
- | @Z_geb, _
- | @Z_gtb, _
- | @Z_of_nat, _
- | @Z_to_nat, _
- | @Z_shiftr, _
- | @Z_shiftl, _
- | @Z_land, _
- | @Z_lor, _
- | @Z_min, _
- | @Z_max, _
- | @Z_bneg, _
- | @Z_lnot_modulo, _
- | @Z_mul_split, _
- | @Z_add_get_carry, _
- | @Z_add_with_carry, _
- | @Z_add_with_get_carry, _
- | @Z_sub_get_borrow, _
- | @Z_sub_with_get_borrow, _
- | @Z_zselect, _
- | @Z_add_modulo, _
- | @Z_rshi, _
- | @Z_cc_m, _
- | @Z_combine_at_bitwidth, _
- | @Z_cast, _
- | @Z_cast2, _
- | @option_Some _, _
- | @option_None _, _
- | @option_rect _ _, _
- | @Build_zrange, _
- | @zrange_rect _, _
- | @fancy_add, _
- | @fancy_addc, _
- | @fancy_sub, _
- | @fancy_subb, _
- | @fancy_mulll, _
- | @fancy_mullh, _
- | @fancy_mulhl, _
- | @fancy_mulhh, _
- | @fancy_rshi, _
- | @fancy_selc, _
- | @fancy_selm, _
- | @fancy_sell, _
- | @fancy_addm, _
- => Datatypes.None
- end%cps.
-
- Definition of_typed_ident {t} (idc : Compilers.ident.ident t) : ident (type.relax t)
- := match idc with
- | Compilers.ident.Literal t v => @Literal t
- | Compilers.ident.Nat_succ => @Nat_succ
- | Compilers.ident.Nat_pred => @Nat_pred
- | Compilers.ident.Nat_max => @Nat_max
- | Compilers.ident.Nat_mul => @Nat_mul
- | Compilers.ident.Nat_add => @Nat_add
- | Compilers.ident.Nat_sub => @Nat_sub
- | Compilers.ident.Nat_eqb => @Nat_eqb
- | Compilers.ident.nil t => @nil (base.relax t)
- | Compilers.ident.cons t => @cons (base.relax t)
- | Compilers.ident.pair A B => @pair (base.relax A) (base.relax B)
- | Compilers.ident.fst A B => @fst (base.relax A) (base.relax B)
- | Compilers.ident.snd A B => @snd (base.relax A) (base.relax B)
- | Compilers.ident.prod_rect A B T => @prod_rect (base.relax A) (base.relax B) (base.relax T)
- | Compilers.ident.bool_rect T => @bool_rect (base.relax T)
- | Compilers.ident.nat_rect P => @nat_rect (base.relax P)
- | Compilers.ident.nat_rect_arrow P Q => @nat_rect_arrow (base.relax P) (base.relax Q)
- | 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)
- | Compilers.ident.List_length T => @List_length (base.relax T)
- | Compilers.ident.List_seq => @List_seq
- | Compilers.ident.List_firstn A => @List_firstn (base.relax A)
- | Compilers.ident.List_skipn A => @List_skipn (base.relax A)
- | Compilers.ident.List_repeat A => @List_repeat (base.relax A)
- | Compilers.ident.List_combine A B => @List_combine (base.relax A) (base.relax B)
- | Compilers.ident.List_map A B => @List_map (base.relax A) (base.relax B)
- | Compilers.ident.List_app A => @List_app (base.relax A)
- | Compilers.ident.List_rev A => @List_rev (base.relax A)
- | Compilers.ident.List_flat_map A B => @List_flat_map (base.relax A) (base.relax B)
- | Compilers.ident.List_partition A => @List_partition (base.relax A)
- | Compilers.ident.List_fold_right A B => @List_fold_right (base.relax A) (base.relax B)
- | Compilers.ident.List_update_nth T => @List_update_nth (base.relax T)
- | Compilers.ident.List_nth_default T => @List_nth_default (base.relax T)
- | Compilers.ident.eager_List_nth_default T => @eager_List_nth_default (base.relax T)
- | Compilers.ident.Z_add => @Z_add
- | Compilers.ident.Z_mul => @Z_mul
- | Compilers.ident.Z_pow => @Z_pow
- | Compilers.ident.Z_sub => @Z_sub
- | Compilers.ident.Z_opp => @Z_opp
- | Compilers.ident.Z_div => @Z_div
- | Compilers.ident.Z_modulo => @Z_modulo
- | Compilers.ident.Z_log2 => @Z_log2
- | Compilers.ident.Z_log2_up => @Z_log2_up
- | Compilers.ident.Z_eqb => @Z_eqb
- | Compilers.ident.Z_leb => @Z_leb
- | Compilers.ident.Z_ltb => @Z_ltb
- | Compilers.ident.Z_geb => @Z_geb
- | Compilers.ident.Z_gtb => @Z_gtb
- | Compilers.ident.Z_of_nat => @Z_of_nat
- | Compilers.ident.Z_to_nat => @Z_to_nat
- | Compilers.ident.Z_shiftr => @Z_shiftr
- | Compilers.ident.Z_shiftl => @Z_shiftl
- | Compilers.ident.Z_land => @Z_land
- | Compilers.ident.Z_lor => @Z_lor
- | Compilers.ident.Z_min => @Z_min
- | Compilers.ident.Z_max => @Z_max
- | Compilers.ident.Z_bneg => @Z_bneg
- | Compilers.ident.Z_lnot_modulo => @Z_lnot_modulo
- | Compilers.ident.Z_mul_split => @Z_mul_split
- | Compilers.ident.Z_add_get_carry => @Z_add_get_carry
- | Compilers.ident.Z_add_with_carry => @Z_add_with_carry
- | Compilers.ident.Z_add_with_get_carry => @Z_add_with_get_carry
- | Compilers.ident.Z_sub_get_borrow => @Z_sub_get_borrow
- | Compilers.ident.Z_sub_with_get_borrow => @Z_sub_with_get_borrow
- | Compilers.ident.Z_zselect => @Z_zselect
- | Compilers.ident.Z_add_modulo => @Z_add_modulo
- | Compilers.ident.Z_rshi => @Z_rshi
- | Compilers.ident.Z_cc_m => @Z_cc_m
- | Compilers.ident.Z_combine_at_bitwidth => @Z_combine_at_bitwidth
- | Compilers.ident.Z_cast range => @Z_cast
- | Compilers.ident.Z_cast2 range => @Z_cast2
- | Compilers.ident.option_Some A => @option_Some (base.relax A)
- | Compilers.ident.option_None A => @option_None (base.relax A)
- | Compilers.ident.option_rect A P => @option_rect (base.relax A) (base.relax P)
- | Compilers.ident.Build_zrange => @Build_zrange
- | Compilers.ident.zrange_rect P => @zrange_rect (base.relax P)
- | Compilers.ident.fancy_add log2wordmax imm => @fancy_add
- | Compilers.ident.fancy_addc log2wordmax imm => @fancy_addc
- | Compilers.ident.fancy_sub log2wordmax imm => @fancy_sub
- | Compilers.ident.fancy_subb log2wordmax imm => @fancy_subb
- | Compilers.ident.fancy_mulll log2wordmax => @fancy_mulll
- | Compilers.ident.fancy_mullh log2wordmax => @fancy_mullh
- | Compilers.ident.fancy_mulhl log2wordmax => @fancy_mulhl
- | Compilers.ident.fancy_mulhh log2wordmax => @fancy_mulhh
- | Compilers.ident.fancy_rshi log2wordmax x => @fancy_rshi
- | Compilers.ident.fancy_selc => @fancy_selc
- | Compilers.ident.fancy_selm log2wordmax => @fancy_selm
- | Compilers.ident.fancy_sell => @fancy_sell
- | Compilers.ident.fancy_addm => @fancy_addm
+ Definition relax_kind_of_type {T} : Raw.ident.Type_of_kind_of_type T -> Type_of_kind_of_type T
+ := match T with
+ | Raw.ident.GallinaType _
+ | Raw.ident.BaseBaseType
+ => fun x => x
+ | Raw.ident.BaseType => pattern.base.relax
end.
-
- Definition arg_types_of_typed_ident {t} (idc : Compilers.ident.ident t) : type_of_list (arg_types (of_typed_ident idc))
- := match idc in Compilers.ident.ident t return type_of_list (arg_types (of_typed_ident idc)) with
- | Compilers.ident.Literal t v => (v, tt)
- | Compilers.ident.Nat_succ => tt
- | Compilers.ident.Nat_pred => tt
- | Compilers.ident.Nat_max => tt
- | Compilers.ident.Nat_mul => tt
- | Compilers.ident.Nat_add => tt
- | Compilers.ident.Nat_sub => tt
- | Compilers.ident.Nat_eqb => tt
- | Compilers.ident.nil t => tt
- | Compilers.ident.cons t => tt
- | Compilers.ident.pair A B => tt
- | Compilers.ident.fst A B => tt
- | Compilers.ident.snd A B => tt
- | Compilers.ident.prod_rect A B T => tt
- | Compilers.ident.bool_rect T => tt
- | Compilers.ident.nat_rect P => tt
- | Compilers.ident.nat_rect_arrow P Q => tt
- | 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
- | Compilers.ident.List_length T => tt
- | Compilers.ident.List_seq => tt
- | Compilers.ident.List_firstn A => tt
- | Compilers.ident.List_skipn A => tt
- | Compilers.ident.List_repeat A => tt
- | Compilers.ident.List_combine A B => tt
- | Compilers.ident.List_map A B => tt
- | Compilers.ident.List_app A => tt
- | Compilers.ident.List_rev A => tt
- | Compilers.ident.List_flat_map A B => tt
- | Compilers.ident.List_partition A => tt
- | Compilers.ident.List_fold_right A B => tt
- | Compilers.ident.List_update_nth T => tt
- | Compilers.ident.List_nth_default T => tt
- | Compilers.ident.eager_List_nth_default T => tt
- | Compilers.ident.Z_add => tt
- | Compilers.ident.Z_mul => tt
- | Compilers.ident.Z_pow => tt
- | Compilers.ident.Z_sub => tt
- | Compilers.ident.Z_opp => tt
- | Compilers.ident.Z_div => tt
- | Compilers.ident.Z_modulo => tt
- | Compilers.ident.Z_log2 => tt
- | Compilers.ident.Z_log2_up => tt
- | Compilers.ident.Z_eqb => tt
- | Compilers.ident.Z_leb => tt
- | Compilers.ident.Z_ltb => tt
- | Compilers.ident.Z_geb => tt
- | Compilers.ident.Z_gtb => tt
- | Compilers.ident.Z_of_nat => tt
- | Compilers.ident.Z_to_nat => tt
- | Compilers.ident.Z_shiftr => tt
- | Compilers.ident.Z_shiftl => tt
- | Compilers.ident.Z_land => tt
- | Compilers.ident.Z_lor => tt
- | Compilers.ident.Z_min => tt
- | Compilers.ident.Z_max => tt
- | Compilers.ident.Z_bneg => tt
- | Compilers.ident.Z_lnot_modulo => tt
- | Compilers.ident.Z_mul_split => tt
- | Compilers.ident.Z_add_get_carry => tt
- | Compilers.ident.Z_add_with_carry => tt
- | Compilers.ident.Z_add_with_get_carry => tt
- | Compilers.ident.Z_sub_get_borrow => tt
- | Compilers.ident.Z_sub_with_get_borrow => tt
- | Compilers.ident.Z_zselect => tt
- | Compilers.ident.Z_add_modulo => tt
- | Compilers.ident.Z_rshi => tt
- | Compilers.ident.Z_cc_m => tt
- | Compilers.ident.Z_combine_at_bitwidth => tt
- | Compilers.ident.Z_cast range => (range, tt)
- | Compilers.ident.Z_cast2 range => (range, tt)
- | Compilers.ident.option_Some A => tt
- | Compilers.ident.option_None A => tt
- | Compilers.ident.option_rect A P => tt
- | Compilers.ident.Build_zrange => tt
- | Compilers.ident.zrange_rect P => tt
- | Compilers.ident.fancy_add log2wordmax imm => (log2wordmax, (imm, tt))
- | Compilers.ident.fancy_addc log2wordmax imm => (log2wordmax, (imm, tt))
- | Compilers.ident.fancy_sub log2wordmax imm => (log2wordmax, (imm, tt))
- | Compilers.ident.fancy_subb log2wordmax imm => (log2wordmax, (imm, tt))
- | Compilers.ident.fancy_mulll log2wordmax => (log2wordmax, tt)
- | Compilers.ident.fancy_mullh log2wordmax => (log2wordmax, tt)
- | Compilers.ident.fancy_mulhl log2wordmax => (log2wordmax, tt)
- | Compilers.ident.fancy_mulhh log2wordmax => (log2wordmax, tt)
- | Compilers.ident.fancy_rshi log2wordmax x => (log2wordmax, (x, tt))
- | Compilers.ident.fancy_selc => tt
- | Compilers.ident.fancy_selm log2wordmax => (log2wordmax, tt)
- | Compilers.ident.fancy_sell => tt
- | Compilers.ident.fancy_addm => tt
+ Definition subst_default_kind_of_type (evm : EvarMap) {T} : Type_of_kind_of_type T -> Raw.ident.Type_of_kind_of_type T
+ := match T with
+ | Raw.ident.GallinaType _
+ | Raw.ident.BaseBaseType
+ => fun x => x
+ | Raw.ident.BaseType => fun t => pattern.base.subst_default t evm
end.
- Derive type_of_list_arg_types_beq
- SuchThat (forall {t idc}, reflect_rel (@eq (type_of_list (@arg_types t idc))) (@type_of_list_arg_types_beq t idc))
- As reflect_type_of_list_arg_types_beq.
- Proof.
- subst type_of_list_arg_types_beq; intros t idc.
- instantiate (1:=ltac:(intros t idc; destruct idc)); destruct idc; cbn [fold_right arg_types]; try solve [ exact reflect_eq_unit ]; instantiate (1:=ltac:(cbn [fold_right arg_types])); exact _.
- Qed.
- End ident.
-
- (*===*)
+ Local Notation dep_types := Raw.ident.dep_types.
+ Local Notation preinfos := Raw.ident.preinfos.
+ Local Notation ident_infos_of := Raw.ident.ident_infos_of.
+ Local Notation indep_types := Raw.ident.indep_types.
+ Local Notation indep_args := Raw.ident.indep_args.
+ Local Notation iffT A B := ((A -> B) * (B -> A))%type.
+
+ Ltac collect_args' f cur :=
+ lazymatch f with
+ | ?f ?x => collect_args' f (x, cur)
+ | _ => cur
+ end.
+ Ltac collect_args f := collect_args' f Datatypes.tt.
+
+ Ltac build_split_types :=
+ let t := fresh "t" in
+ let idc := fresh "idc" in
+ let idc' := fresh "idc'" in
+ let v := constr:(
+ fun t (idc : ident t)
+ => let idc' := idc in
+ ltac:(destruct idc;
+ let idc := (eval cbv [idc'] in idc') in
+ let ctor := head idc in
+ let all_idents := (eval cbv [all_idents] in all_idents) in
+ let all_ridents := (eval cbv [Raw.ident.all_idents] in Raw.ident.all_idents) in
+ let v := find_ctor ctor all_idents all_ridents in
+ let args := collect_args idc in
+ let f := (eval cbv [list_unapp_type_of_list dep_types preinfos ident_infos_of indep_types List.app List.map Type_of_kind_of_type] in
+ (@list_unapp_type_of_list
+ (dep_types (preinfos (ident_infos_of v)))
+ (List.map Type_of_kind_of_type (indep_types (preinfos (ident_infos_of v)))))) in
+ refine (existT
+ _
+ v
+ (f args)))
+ : { ridc : Raw.ident & type_of_list (dep_types (preinfos (ident_infos_of ridc))) * type_of_list_of_kind (indep_types (preinfos (ident_infos_of ridc))) }%type) in
+ let v := (eval cbn [Datatypes.fst Datatypes.snd] in v) in
+ v.
+ Ltac make_split_types := let v := build_split_types in refine v.
+
+ Ltac build_add_types_from_raw_sig split_types :=
+ let ridc := fresh "ridc" in
+ let ridc' := fresh "ridc'" in
+ let dt := fresh "dt" in
+ let idt := fresh "idt" in
+ let v := (eval cbv [id] in
+ (fun (ridc : Raw.ident)
+ (dt : type_of_list (dep_types (preinfos (ident_infos_of ridc))))
+ (idt : type_of_list_of_kind (indep_types (preinfos (ident_infos_of ridc))))
+ => let ridc' := ridc in
+ ltac:(destruct ridc;
+ let ridc := (eval cbv [ridc'] in ridc') in
+ let all_idents := (eval cbv [all_idents] in all_idents) in
+ let all_ridents := (eval cbv [Raw.ident.all_idents] in Raw.ident.all_idents) in
+ let v := find_ctor ridc all_ridents all_idents in
+ let v := (eval cbv [projT2] in (projT2 v)) in
+ eexists;
+ unshelve eexists;
+ [ eapply v
+ | cbv [split_types]; apply f_equal;
+ repeat match goal with
+ | [ |- (_, _) = _ ] => apply Prod.path_prod; cbn [Datatypes.fst Datatypes.snd]
+ | [ |- Datatypes.tt = ?x ] => destruct x; reflexivity
+ | [ |- ?ev = _ ] => is_evar ev; reflexivity
+ end ])
+ : { t : _ & { idc : ident t | @split_types _ idc = existT _ ridc (dt, idt) } })) in
+ v.
+ Ltac make_add_types_from_raw_sig split_types :=
+ let v := build_add_types_from_raw_sig split_types in refine v.
+
+ Definition split_types : forall {t} (idc : ident t), { ridc : Raw.ident & type_of_list (dep_types (preinfos (ident_infos_of ridc))) * type_of_list_of_kind (indep_types (preinfos (ident_infos_of ridc))) }%type
+ := ltac:(make_split_types).
+
+ Definition add_types_from_raw_sig
+ : forall (ridc : Raw.ident)
+ (dt : type_of_list (dep_types (preinfos (ident_infos_of ridc))))
+ (idt : type_of_list_of_kind (indep_types (preinfos (ident_infos_of ridc)))),
+ { t : _ & { idc : ident t | @split_types _ idc = existT _ ridc (dt, idt) } }
+ := ltac:(make_add_types_from_raw_sig (@split_types)).
+
+ 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).
+ 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).
+ 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).
+ 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
+ (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))))))))).
+ 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))) 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).
+ End ident.
End pattern.
End Compilers.
diff --git a/src/GENERATEDIdentifiersWithoutTypesProofs.v b/src/GENERATEDIdentifiersWithoutTypesProofs.v
index 9094a8a98..2bab688dc 100644
--- a/src/GENERATEDIdentifiersWithoutTypesProofs.v
+++ b/src/GENERATEDIdentifiersWithoutTypesProofs.v
@@ -84,7 +84,8 @@ Module Compilers.
Import GENERATEDIdentifiersWithoutTypes.Compilers.pattern.Raw.ident.
Import Datatypes. (* for Some, None, option *)
- Global Instance eq_ident_Decidable : DecidableRel (@eq ident) := ident_eq_dec.
+ Global Instance eq_ident_Decidable : DecidableRel (@eq ident)
+ := dec_rel_of_bool_dec_rel ident_beq ident_bl ident_lb.
Lemma to_typed_invert_bind_args_gen t idc p f
: @invert_bind_args t idc p = Some f
@@ -116,30 +117,45 @@ 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).
Proof.
- split; intro H;
- [ | specialize (fun f1 f2 => H _ (@to_typed p f1) _ (@to_typed p f2)) ];
- destruct p; cbn in *; try solve [ reflexivity | exfalso; discriminate ];
- repeat first [ progress intros *
- | match goal with
- | [ |- ?x = ?x ] => reflexivity
- | [ |- ?x = ?x -> _ ] => intros _
- | [ |- None <> None -> ?P ] => exact (@quick_invert_neq_option _ P None None)
- | [ |- Some _ <> None -> _ ] => intros _
- | [ |- None <> Some _ -> _ ] => intros _
- | [ H : forall x y, Some _ <> None -> _ |- _ ] => specialize (fun x y => H x y Some_neq_None)
- | [ 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
- | break_innermost_match_step
- | congruence ].
+ rewrite is_simple_correct0; split; intro H.
+ { intros t1 idc1 t2 idc2 H1 H2.
+ destruct (invert_bind_args idc1 p) eqn:?, (invert_bind_args idc2 p) eqn:?; try congruence.
+ erewrite (type_of_invert_bind_args t1), (type_of_invert_bind_args t2) by eassumption.
+ apply H. }
+ { intros f1 f2.
+ apply (H _ (to_typed p f1) _ (to_typed p f2));
+ rewrite invert_bind_args_to_typed; congruence. }
Qed.
End ident.
End Raw.
@@ -152,13 +168,6 @@ Module Compilers.
: @eta_ident_cps T t idc f = f t idc.
Proof. cbv [eta_ident_cps]; break_innermost_match; reflexivity. Qed.
-(*
- Lemma is_simple_strip_types_iff_type_vars_nil {t} idc
- : Raw.ident.is_simple (@strip_types t idc) = true
- <-> type_vars idc = List.nil.
- Proof. destruct idc; cbn; intuition congruence. Qed.
-*)
-
Lemma unify_to_typed {t t' pidc idc}
: forall v,
@unify t t' pidc idc = Some v
@@ -180,30 +189,6 @@ Module Compilers.
Proof.
destruct idc; cbn; break_innermost_match; exact Some_neq_None.
Qed.
-
- Lemma to_typed_of_typed_ident {t idc}
- : forall v,
- unify (@of_typed_ident t idc) idc = Some v
- -> forall evm pf,
- (rew [Compilers.ident] pf in to_typed (@of_typed_ident t idc) evm v)
- = idc.
- Proof.
- destruct idc.
- all: repeat first [ break_innermost_match_step
- | break_innermost_match_hyps_step
- | progress intros
- | reflexivity
- | progress subst
- | progress inversion_option
- | progress eliminate_hprop_eq
- | progress fold (@base.subst_default)
- | progress cbn in *
- | lazymatch goal with
- | [ H : context[base.subst_default (base.relax ?t) ?evm] |- _ ]
- => generalize dependent (base.subst_default (base.relax t) evm)
- end
- | progress Compilers.type.inversion_type ].
- Qed.
End ident.
End pattern.
End Compilers.
diff --git a/src/Rewriter.v b/src/Rewriter.v
index 34107b2c2..e1b537959 100644
--- a/src/Rewriter.v
+++ b/src/Rewriter.v
@@ -531,23 +531,6 @@ Module Compilers.
(fun T Ts rec f1 f2 => forall x, rec (f1 x) (f2 x))
ls.
- Definition app_type_of_list {K} {ls : list Type} (f : type_of_list_cps K ls) (args : type_of_list ls) : K
- := list_rect
- (fun ls
- => type_of_list_cps K ls -> type_of_list ls -> K)
- (fun v _ => v)
- (fun T Ts rec f x
- => rec (f (fst x)) (snd x))
- ls
- f args.
-
- Definition lam_type_of_list {ls K} : (type_of_list ls -> K) -> type_of_list_cps K ls
- := list_rect
- (fun ls => (type_of_list ls -> K) -> type_of_list_cps K ls)
- (fun f => f tt)
- (fun T Ts rec k t => rec (fun ts => k (t, ts)))
- ls.
-
Local Notation "e <---- e' ; f" := (splice_value_with_lets e' (fun e => f%under_lets)) : under_lets_scope.
Local Notation "e <----- e' ; f" := (splice_under_lets_with_value e' (fun e => f%under_lets)) : under_lets_scope.
@@ -2154,6 +2137,12 @@ Module Compilers.
:= Eval cbv [pattern.ident.of_typed_ident] in
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
+ (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).
+
Fixpoint make_Literal_pattern (t : pattern.base.type) : option (pattern t)
:= match t return option (pattern t) with
| pattern.base.type.var _ => None
@@ -2161,7 +2150,7 @@ Module Compilers.
| pattern.base.type.prod A B
=> (a <- make_Literal_pattern A;
b <- make_Literal_pattern B;
- Some ((#pattern.ident.pair @ a @ b)%pattern))
+ Some ((#(pident_pair _ _) @ a @ b)%pattern))
| pattern.base.type.list A => None
| pattern.base.type.option A => None
end%option%cps.