diff options
Diffstat (limited to 'src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v')
| -rw-r--r-- | src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v | 1741 |
1 files changed, 1741 insertions, 0 deletions
diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v new file mode 100644 index 000000000..94257f793 --- /dev/null +++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v @@ -0,0 +1,1741 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.CPSNotations. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Experiments.NewPipeline.Language. + +Module Compilers. + Export Language.Compilers. + + Module pattern. + Module ident. + Set Boolean Equality Schemes. + (*Print Compilers.ident.ident.*) + (*Show Match Compilers.ident.ident.*) + (* +<<< +#!/usr/bin/env python2 +import re + +print_ident = r"""Inductive ident : Compilers.type Compilers.base.type.type -> Set := + Literal : forall t : base.type.base, + base.interp (Compilers.base.type.type_base t) -> + ident ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base t)) + | Nat_succ : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat))%etype + | Nat_pred : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat))%etype + | Nat_max : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat))%etype + | Nat_mul : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat))%etype + | Nat_add : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat))%etype + | Nat_sub : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat))%etype + | nil : forall t : Compilers.base.type.type, ident ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list t)) + | cons : forall t : Compilers.base.type.type, + ident + ((fun x : Compilers.base.type.type => type.base x) t -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list t) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list t))%etype + | pair : forall A B : Compilers.base.type.type, + ident + ((fun x : Compilers.base.type.type => type.base x) A -> + (fun x : Compilers.base.type.type => type.base x) B -> (fun x : Compilers.base.type.type => type.base x) (A * B)%etype)%etype + | fst : forall A B : Compilers.base.type.type, + ident + ((fun x : Compilers.base.type.type => type.base x) (A * B)%etype -> (fun x : Compilers.base.type.type => type.base x) A)%etype + | snd : forall A B : Compilers.base.type.type, + ident + ((fun x : Compilers.base.type.type => type.base x) (A * B)%etype -> (fun x : Compilers.base.type.type => type.base x) B)%etype + | pair_rect : forall A B T : Compilers.base.type.type, + ident + (((fun x : Compilers.base.type.type => type.base x) A -> + (fun x : Compilers.base.type.type => type.base x) B -> (fun x : Compilers.base.type.type => type.base x) T) -> + (fun x : Compilers.base.type.type => type.base x) (A * B)%etype -> + (fun x : Compilers.base.type.type => type.base x) T)%etype + | bool_rect : forall T : Compilers.base.type.type, + ident + (((fun x : Compilers.base.type.type => type.base x) ()%etype -> (fun x : Compilers.base.type.type => type.base x) T) -> + ((fun x : Compilers.base.type.type => type.base x) ()%etype -> (fun x : Compilers.base.type.type => type.base x) T) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.bool) -> + (fun x : Compilers.base.type.type => type.base x) T)%etype + | nat_rect : forall P : Compilers.base.type.type, + ident + (((fun x : Compilers.base.type.type => type.base x) ()%etype -> (fun x : Compilers.base.type.type => type.base x) P) -> + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) P -> (fun x : Compilers.base.type.type => type.base x) P) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) P)%etype + | list_rect : forall A P : Compilers.base.type.type, + ident + (((fun x : Compilers.base.type.type => type.base x) ()%etype -> (fun x : Compilers.base.type.type => type.base x) P) -> + ((fun x : Compilers.base.type.type => type.base x) A -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list A) -> + (fun x : Compilers.base.type.type => type.base x) P -> (fun x : Compilers.base.type.type => type.base x) P) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list A) -> + (fun x : Compilers.base.type.type => type.base x) P)%etype + | list_case : forall A P : Compilers.base.type.type, + ident + (((fun x : Compilers.base.type.type => type.base x) ()%etype -> (fun x : Compilers.base.type.type => type.base x) P) -> + ((fun x : Compilers.base.type.type => type.base x) A -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list A) -> + (fun x : Compilers.base.type.type => type.base x) P) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list A) -> + (fun x : Compilers.base.type.type => type.base x) P)%etype + | List_length : forall T : Compilers.base.type.type, + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list T) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat))%etype + | List_seq : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) + (Compilers.base.type.list (Compilers.base.type.type_base base.type.nat)))%etype + | List_repeat : forall A : Compilers.base.type.type, + ident + ((fun x : Compilers.base.type.type => type.base x) A -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list A))%etype + | List_combine : forall A B : Compilers.base.type.type, + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list A) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list B) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list (A * B)))%etype + | List_map : forall A B : Compilers.base.type.type, + ident + (((fun x : Compilers.base.type.type => type.base x) A -> (fun x : Compilers.base.type.type => type.base x) B) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list A) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list B))%etype + | List_app : forall A : Compilers.base.type.type, + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list A) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list A) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list A))%etype + | List_rev : forall A : Compilers.base.type.type, + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list A) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list A))%etype + | List_flat_map : forall A B : Compilers.base.type.type, + ident + (((fun x : Compilers.base.type.type => type.base x) A -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list B)) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list A) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list B))%etype + | List_partition : forall A : Compilers.base.type.type, + ident + (((fun x : Compilers.base.type.type => type.base x) A -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.bool)) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list A) -> + (fun x : Compilers.base.type.type => type.base x) + (Compilers.base.type.list A * Compilers.base.type.list A)%etype)%etype + | List_fold_right : forall A B : Compilers.base.type.type, + ident + (((fun x : Compilers.base.type.type => type.base x) B -> + (fun x : Compilers.base.type.type => type.base x) A -> (fun x : Compilers.base.type.type => type.base x) A) -> + (fun x : Compilers.base.type.type => type.base x) A -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list B) -> + (fun x : Compilers.base.type.type => type.base x) A)%etype + | List_update_nth : forall T : Compilers.base.type.type, + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + ((fun x : Compilers.base.type.type => type.base x) T -> (fun x : Compilers.base.type.type => type.base x) T) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list T) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list T))%etype + | List_nth_default : forall T : Compilers.base.type.type, + ident + ((fun x : Compilers.base.type.type => type.base x) T -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.list T) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) T)%etype + | Z_add : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_mul : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_pow : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_sub : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_opp : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_div : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_modulo : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_eqb : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.bool))%etype + | Z_leb : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.bool))%etype + | Z_of_nat : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.nat) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_shiftr : Z -> + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_shiftl : Z -> + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_land : Z -> + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_mul_split : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | Z_mul_split_concrete : Z -> + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | Z_add_get_carry : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | Z_add_get_carry_concrete : Z -> + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | Z_add_with_carry : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_add_with_get_carry : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | Z_add_with_get_carry_concrete : Z -> + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | Z_sub_get_borrow : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | Z_sub_get_borrow_concrete : Z -> + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | Z_sub_with_get_borrow : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | Z_sub_with_get_borrow_concrete : Z -> + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | Z_zselect : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_add_modulo : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_rshi : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_rshi_concrete : Z -> + Z -> + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_cc_m : ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_cc_m_concrete : Z -> + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_neg_snd : ident + ((fun x : Compilers.base.type.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 => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | Z_cast : zrange -> + ident + ((fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z) -> + (fun x : Compilers.base.type.type => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | Z_cast2 : zrange * zrange -> + ident + ((fun x : Compilers.base.type.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 => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | fancy_add : Z -> + Z -> + ident + ((fun x : Compilers.base.type.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 => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | fancy_addc : Z -> + Z -> + ident + ((fun x : Compilers.base.type.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 => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | fancy_sub : Z -> + Z -> + ident + ((fun x : Compilers.base.type.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 => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | fancy_subb : Z -> + Z -> + ident + ((fun x : Compilers.base.type.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 => type.base x) + (Compilers.base.type.type_base base.type.Z * Compilers.base.type.type_base base.type.Z)%etype)%etype + | fancy_mulll : Z -> + ident + ((fun x : Compilers.base.type.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 => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | fancy_mullh : Z -> + ident + ((fun x : Compilers.base.type.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 => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | fancy_mulhl : Z -> + ident + ((fun x : Compilers.base.type.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 => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | fancy_mulhh : Z -> + ident + ((fun x : Compilers.base.type.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 => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | fancy_rshi : Z -> + Z -> + ident + ((fun x : Compilers.base.type.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 => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | fancy_selc : ident + ((fun x : Compilers.base.type.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 => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | fancy_selm : Z -> + ident + ((fun x : Compilers.base.type.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 => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | fancy_sell : ident + ((fun x : Compilers.base.type.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 => type.base x) (Compilers.base.type.type_base base.type.Z))%etype + | fancy_addm : ident + ((fun x : Compilers.base.type.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 => type.base x) (Compilers.base.type.type_base base.type.Z))%etype +""" +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.nil t => + | ident.cons t => + | ident.pair A B => + | ident.fst A B => + | ident.snd A B => + | ident.pair_rect A B T => + | ident.bool_rect T => + | ident.nat_rect P => + | ident.list_rect A P => + | ident.list_case A P => + | ident.List_length T => + | ident.List_seq => + | 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.Z_add => + | ident.Z_mul => + | ident.Z_pow => + | ident.Z_sub => + | ident.Z_opp => + | ident.Z_div => + | ident.Z_modulo => + | ident.Z_eqb => + | ident.Z_leb => + | ident.Z_of_nat => + | ident.Z_shiftr offset => + | ident.Z_shiftl offset => + | ident.Z_land mask => + | ident.Z_mul_split => + | ident.Z_mul_split_concrete s => + | ident.Z_add_get_carry => + | ident.Z_add_get_carry_concrete s => + | ident.Z_add_with_carry => + | ident.Z_add_with_get_carry => + | ident.Z_add_with_get_carry_concrete s => + | ident.Z_sub_get_borrow => + | ident.Z_sub_get_borrow_concrete s => + | ident.Z_sub_with_get_borrow => + | ident.Z_sub_with_get_borrow_concrete s => + | ident.Z_zselect => + | ident.Z_add_modulo => + | ident.Z_rshi => + | ident.Z_rshi_concrete s offset => + | ident.Z_cc_m => + | ident.Z_cc_m_concrete s => + | ident.Z_neg_snd => + | ident.Z_cast range => + | ident.Z_cast2 range => + | 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 + +""" +prefix = 'Compilers.' +indent = ' ' +exts = ('Unit', 'Z', 'Bool', 'Nat') +tys = [('%sbase.type.' % prefix) + i for i in ('unit', 'Z', 'bool', 'nat')] +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()]) +ttypes = ([[] for ty in tys] + + [get_dep_types(case) + for case in print_ident.replace('\n', ' ').split('|')[1:]]) +ctypes = ([['base.interp ' + ty] for ty in tys] + + [[i.strip() for i in re.sub(r'forall [^:]+ : %sbase.type.type,' % prefix, '', i[i.find(':')+1:i.find('ident')]).strip(' ->').split('->') if i.strip()] + for i in print_ident.replace('\n', ' ').split('|')[1:]]) +crettypes = ([('%sident.ident (type.base (%sbase.type.type_base ' + ty + '))') % (prefix, prefix) for ty in tys] + + [prefix + 'ident.' + re.sub(r'\(fun x : [^ ]+ => ([^ ]+) x\)', r'\1', re.sub(' +', ' ', i[i.find('ident'):])) + for i in print_ident.replace('\n', ' ').split('|')[1:]]) + +retcode = r"""Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.CPSNotations. +Require Import Crypto.Util.ZRange. +Require Import Crypto.Experiments.NewPipeline.Language. + +Module Compilers. + Export Language.Compilers. + + Module pattern. + Module ident. + Set Boolean Equality Schemes. + (*Print Compilers.ident.ident.*) + (*Show Match Compilers.ident.ident.*) +""" + +def addnewline(s): return s + '\n' + +retcode += addnewline(r"""%s(* +<<< +%s +>>> +%s*) +""" % (indent, open(__file__).read(), indent)) +retcode += addnewline(r"""%sInductive ident := +%s| %s. +""" % (indent, indent, ('\n' + indent + '| ').join(pctors))) +#retcode += addnewline((r"""%sDefinition beq_typed {t} (X : ident) (Y : %sident.ident t) : bool +# := match X, Y with +# | %s +# => true +# | %s +# => false +# end. +#""" % (indent, prefix, +# '\n | '.join(pctor + ', ' + ' '.join([ctor[0]] + ['_'] * (len(ctor)-1)) +# for pctor, ctor in zip(pctors, ctors_with_prefix)), +# '\n | '.join(pctor + ', _' for pctor in pctors))).replace('\n', '\n' + indent)) +retcode += addnewline((r"""%sDefinition try_make_transport_ident_cps (P : ident -> Type) (idc1 idc2 : ident) : ~> option (P idc1 -> P idc2) + := match idc1, idc2 with + | %s + => fun T k => k (Some (fun v => v)) + | %s + => fun T k => k None + end%%cps. +""" % (indent, + '\n | '.join(pctor + ', ' + pctor for pctor in pctors), + '\n | '.join(pctor + ', _' for pctor in pctors))).replace('\n', '\n' + indent)) +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. +""" % (indent, 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' + indent)) +#retcode += addnewline((r"""%sDefinition eta_all_option_cps {T} (f : ident -> option T) +# : option (ident -> T) +# := (%s; +# Some (fun c +# => match c with +# | %s +# end))%%option. +#""" % (indent, +# ';\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' + indent)) +retcode += addnewline((r"""%sDefinition of_typed_ident {t} (idc : %sident.ident t) : ident + := match idc with + | %s + end. +""" % (indent, prefix, '\n | '.join(' '.join(ctor) + ' => ' + pctor for ctor, pctor in zip(ctors_with_prefix, pctors)))).replace('\n', '\n' + indent)) +#retcode += addnewline((r"""%sDefinition orb (f : ident -> bool) : bool +# := (%s)%%bool. +#""" % (indent, ' || '.join('f ' + pctor for pctor in pctors))).replace('\n', '\n' + indent)) +retcode += addnewline((r"""%sDefinition arg_types (idc : ident) : option %s + := match idc return option %s with + | %s + end%%type. +""" % (indent, type_or_set, type_or_set, + '\n | '.join(pctor + ' => ' + ('None' if len(ctype) == 0 else '@Some ' + type_or_set + ' ' + (ctype[0] if ' ' not in ' * '.join(ctype) else '(%s)' % ' * '.join(ctype))) + for pctor, ctype in zip(pctors, ctypes)))).replace('\n', '\n' + indent)) +retcode += addnewline((r"""%sDefinition full_types (idc : ident) : %s + := match idc return %s with + | %s + end%%type. +""" % (indent, type_or_set, type_or_set, + '\n | '.join(pctor + ' => ' + (' * '.join(ttype + ctype) if len(ttype + ctype) > 0 else 'unit') + for pctor, ttype, ctype in zip(pctors, ttypes, ctypes)))).replace('\n', '\n' + indent)) + +retcode += addnewline((r"""%sDefinition bind_args {t} (idc : %sident.ident t) : match arg_types (of_typed_ident idc) return %s with Some t => t | None => unit end + := match idc return match arg_types (of_typed_ident idc) return %s with Some t => t | None => unit end with + | %s + end%%cps. +""" % (indent, prefix, type_or_set, type_or_set, + '\n | '.join(' '.join(ctor) + ' => ' + ('tt' if len(ctype) == 0 else (ctor[-1] if len(ctype) == 1 else '(%s)' % ', '.join(ctor[-len(ctype):]))) + for ctor, ctype in zip(ctors_with_prefix, ctypes)))).replace('\n', '\n' + indent)) +retcode += addnewline((r"""%sDefinition invert_bind_args {t} (idc : %sident.ident t) (pidc : ident) : option (full_types pidc) + := match pidc, idc return option (full_types pidc) with + | %s + | %s + => None + end%%cps. +""" % (indent, prefix, + '\n | '.join(pctor + ', ' + ' '.join(ctor) + ' => Some ' + ('tt' if len(ttype + ctype) == 0 else (ctor[-1] if len(ttype + ctype) == 1 else '(%s)' % ', '.join(ctor[-len(ttype + ctype):]))) + for pctor, ctor, ttype, ctype in zip(pctors, ctors_with_prefix, ttypes, ctypes)), + '\n | '.join(pctor + ', _' for pctor in pctors))).replace('\n', '\n' + indent)) + +maxeta = max([len(ttype + ctype) for ttype, ctype in zip(ttypes, ctypes)]) +if maxeta >= 2: + retcode += addnewline(r"""%sLocal Notation eta2 x := (Datatypes.fst x, Datatypes.snd x) (only parsing).""" % indent) +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).""" % (indent, 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) : full_types pidc -> %stype %sbase.type + := match pidc return full_types pidc -> _ with + | %s + end. +""" % (indent, prefix, prefix, + '\n | '.join(pctor + ' => ' + + 'fun ' + ('_ => ' if len(ttype + ctype) == 0 else ((ctor[-1] + ' => ') if len(ttype + ctype) == 1 else "arg => let '(%s) := eta%d arg in " % (', '.join(ctor[-len(ttype + ctype):]), 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' + indent)) +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. +""" % (indent, prefix, prefix, + '\n | '.join(pctor + ' => ' + + 'fun ' + (('_ => %s' if len(ttype + ctype) == 0 else ((ctor[-1] + ' => %s') if len(ttype + ctype) == 1 else "arg => match eta%d arg as args' return %sident.ident (type_of %s args') with (%s) => %%s end" % (len(ttype + ctype), prefix, pctor, ', '.join(ctor[-len(ttype + ctype):])))) % ("@" + ' '.join(ctor))) + for pctor, ctor, ttype, ctype in zip(pctors, ctors_with_prefix, ttypes, ctypes)))).replace('\n', '\n' + indent)) +retcode += addnewline((r"""%sDefinition retype_ident {t} (idc : %sident.ident t) : match arg_types (of_typed_ident idc) return %s with Some t => t | None => unit end -> %sident.ident t + := match idc in %sident.ident t return match arg_types (of_typed_ident idc) return %s with Some t => t | None => unit end -> %sident.ident t with + | %s + end. +""" % (indent, 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 Some t => t | 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' + indent)) +# ctor[:len(ctor)-len(ctype)] + ['_'] * len(ctype) + +retcode += addnewline(indent + '\n' + indent + '(*===*)') + +retcode += r""" End ident. + End pattern. +End Compilers. +""" +with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: + f.write(retcode) + +>>> + *) + + Inductive ident := + | LiteralUnit + | LiteralZ + | LiteralBool + | LiteralNat + | Nat_succ + | Nat_pred + | Nat_max + | Nat_mul + | Nat_add + | Nat_sub + | nil + | cons + | pair + | fst + | snd + | pair_rect + | bool_rect + | nat_rect + | list_rect + | list_case + | List_length + | List_seq + | List_repeat + | List_combine + | List_map + | List_app + | List_rev + | List_flat_map + | List_partition + | List_fold_right + | List_update_nth + | List_nth_default + | Z_add + | Z_mul + | Z_pow + | Z_sub + | Z_opp + | Z_div + | Z_modulo + | Z_eqb + | Z_leb + | Z_of_nat + | Z_shiftr + | Z_shiftl + | Z_land + | Z_mul_split + | Z_mul_split_concrete + | Z_add_get_carry + | Z_add_get_carry_concrete + | Z_add_with_carry + | Z_add_with_get_carry + | Z_add_with_get_carry_concrete + | Z_sub_get_borrow + | Z_sub_get_borrow_concrete + | Z_sub_with_get_borrow + | Z_sub_with_get_borrow_concrete + | Z_zselect + | Z_add_modulo + | Z_rshi + | Z_rshi_concrete + | Z_cc_m + | Z_cc_m_concrete + | Z_neg_snd + | Z_cast + | Z_cast2 + | 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. + + Definition try_make_transport_ident_cps (P : ident -> Type) (idc1 idc2 : ident) : ~> option (P idc1 -> P idc2) + := match idc1, idc2 with + | LiteralUnit, LiteralUnit + | LiteralZ, LiteralZ + | LiteralBool, LiteralBool + | LiteralNat, LiteralNat + | Nat_succ, Nat_succ + | Nat_pred, Nat_pred + | Nat_max, Nat_max + | Nat_mul, Nat_mul + | Nat_add, Nat_add + | Nat_sub, Nat_sub + | nil, nil + | cons, cons + | pair, pair + | fst, fst + | snd, snd + | pair_rect, pair_rect + | bool_rect, bool_rect + | nat_rect, nat_rect + | list_rect, list_rect + | list_case, list_case + | List_length, List_length + | List_seq, List_seq + | List_repeat, List_repeat + | List_combine, List_combine + | List_map, List_map + | List_app, List_app + | List_rev, List_rev + | List_flat_map, List_flat_map + | List_partition, List_partition + | List_fold_right, List_fold_right + | List_update_nth, List_update_nth + | List_nth_default, List_nth_default + | Z_add, Z_add + | Z_mul, Z_mul + | Z_pow, Z_pow + | Z_sub, Z_sub + | Z_opp, Z_opp + | Z_div, Z_div + | Z_modulo, Z_modulo + | Z_eqb, Z_eqb + | Z_leb, Z_leb + | Z_of_nat, Z_of_nat + | Z_shiftr, Z_shiftr + | Z_shiftl, Z_shiftl + | Z_land, Z_land + | Z_mul_split, Z_mul_split + | Z_mul_split_concrete, Z_mul_split_concrete + | Z_add_get_carry, Z_add_get_carry + | Z_add_get_carry_concrete, Z_add_get_carry_concrete + | Z_add_with_carry, Z_add_with_carry + | Z_add_with_get_carry, Z_add_with_get_carry + | Z_add_with_get_carry_concrete, Z_add_with_get_carry_concrete + | Z_sub_get_borrow, Z_sub_get_borrow + | Z_sub_get_borrow_concrete, Z_sub_get_borrow_concrete + | Z_sub_with_get_borrow, Z_sub_with_get_borrow + | Z_sub_with_get_borrow_concrete, Z_sub_with_get_borrow_concrete + | Z_zselect, Z_zselect + | Z_add_modulo, Z_add_modulo + | Z_rshi, Z_rshi + | Z_rshi_concrete, Z_rshi_concrete + | Z_cc_m, Z_cc_m + | Z_cc_m_concrete, Z_cc_m_concrete + | Z_neg_snd, Z_neg_snd + | Z_cast, Z_cast + | Z_cast2, Z_cast2 + | fancy_add, fancy_add + | fancy_addc, fancy_addc + | fancy_sub, fancy_sub + | fancy_subb, fancy_subb + | fancy_mulll, fancy_mulll + | fancy_mullh, fancy_mullh + | fancy_mulhl, fancy_mulhl + | fancy_mulhh, fancy_mulhh + | fancy_rshi, fancy_rshi + | fancy_selc, fancy_selc + | fancy_selm, fancy_selm + | fancy_sell, fancy_sell + | fancy_addm, fancy_addm + => fun T k => k (Some (fun v => v)) + | LiteralUnit, _ + | LiteralZ, _ + | LiteralBool, _ + | LiteralNat, _ + | Nat_succ, _ + | Nat_pred, _ + | Nat_max, _ + | Nat_mul, _ + | Nat_add, _ + | Nat_sub, _ + | nil, _ + | cons, _ + | pair, _ + | fst, _ + | snd, _ + | pair_rect, _ + | bool_rect, _ + | nat_rect, _ + | list_rect, _ + | list_case, _ + | List_length, _ + | List_seq, _ + | List_repeat, _ + | List_combine, _ + | List_map, _ + | List_app, _ + | List_rev, _ + | List_flat_map, _ + | List_partition, _ + | List_fold_right, _ + | List_update_nth, _ + | List_nth_default, _ + | Z_add, _ + | Z_mul, _ + | Z_pow, _ + | Z_sub, _ + | Z_opp, _ + | Z_div, _ + | Z_modulo, _ + | Z_eqb, _ + | Z_leb, _ + | Z_of_nat, _ + | Z_shiftr, _ + | Z_shiftl, _ + | Z_land, _ + | Z_mul_split, _ + | Z_mul_split_concrete, _ + | Z_add_get_carry, _ + | Z_add_get_carry_concrete, _ + | Z_add_with_carry, _ + | Z_add_with_get_carry, _ + | Z_add_with_get_carry_concrete, _ + | Z_sub_get_borrow, _ + | Z_sub_get_borrow_concrete, _ + | Z_sub_with_get_borrow, _ + | Z_sub_with_get_borrow_concrete, _ + | Z_zselect, _ + | Z_add_modulo, _ + | Z_rshi, _ + | Z_rshi_concrete, _ + | Z_cc_m, _ + | Z_cc_m_concrete, _ + | Z_neg_snd, _ + | Z_cast, _ + | Z_cast2, _ + | 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, _ + => fun T k => k None + end%cps. + + 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.LiteralUnit v => f _ (@Compilers.ident.LiteralUnit v) + | Compilers.ident.LiteralZ v => f _ (@Compilers.ident.LiteralZ v) + | Compilers.ident.LiteralBool v => f _ (@Compilers.ident.LiteralBool v) + | Compilers.ident.LiteralNat v => f _ (@Compilers.ident.LiteralNat 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.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.pair_rect A B T => f _ (@Compilers.ident.pair_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.list_rect A P => f _ (@Compilers.ident.list_rect A P) + | 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_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.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_eqb => f _ Compilers.ident.Z_eqb + | Compilers.ident.Z_leb => f _ Compilers.ident.Z_leb + | Compilers.ident.Z_of_nat => f _ Compilers.ident.Z_of_nat + | Compilers.ident.Z_shiftr offset => f _ (@Compilers.ident.Z_shiftr offset) + | Compilers.ident.Z_shiftl offset => f _ (@Compilers.ident.Z_shiftl offset) + | Compilers.ident.Z_land mask => f _ (@Compilers.ident.Z_land mask) + | Compilers.ident.Z_mul_split => f _ Compilers.ident.Z_mul_split + | Compilers.ident.Z_mul_split_concrete s => f _ (@Compilers.ident.Z_mul_split_concrete s) + | Compilers.ident.Z_add_get_carry => f _ Compilers.ident.Z_add_get_carry + | Compilers.ident.Z_add_get_carry_concrete s => f _ (@Compilers.ident.Z_add_get_carry_concrete s) + | 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_add_with_get_carry_concrete s => f _ (@Compilers.ident.Z_add_with_get_carry_concrete s) + | Compilers.ident.Z_sub_get_borrow => f _ Compilers.ident.Z_sub_get_borrow + | Compilers.ident.Z_sub_get_borrow_concrete s => f _ (@Compilers.ident.Z_sub_get_borrow_concrete s) + | Compilers.ident.Z_sub_with_get_borrow => f _ Compilers.ident.Z_sub_with_get_borrow + | Compilers.ident.Z_sub_with_get_borrow_concrete s => f _ (@Compilers.ident.Z_sub_with_get_borrow_concrete s) + | 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_rshi_concrete s offset => f _ (@Compilers.ident.Z_rshi_concrete s offset) + | Compilers.ident.Z_cc_m => f _ Compilers.ident.Z_cc_m + | Compilers.ident.Z_cc_m_concrete s => f _ (@Compilers.ident.Z_cc_m_concrete s) + | Compilers.ident.Z_neg_snd => f _ Compilers.ident.Z_neg_snd + | Compilers.ident.Z_cast range => f _ (@Compilers.ident.Z_cast range) + | Compilers.ident.Z_cast2 range => f _ (@Compilers.ident.Z_cast2 range) + | 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. + + Definition of_typed_ident {t} (idc : Compilers.ident.ident t) : ident + := match idc with + | Compilers.ident.LiteralUnit v => LiteralUnit + | Compilers.ident.LiteralZ v => LiteralZ + | Compilers.ident.LiteralBool v => LiteralBool + | Compilers.ident.LiteralNat v => LiteralNat + | 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.nil t => nil + | Compilers.ident.cons t => cons + | Compilers.ident.pair A B => pair + | Compilers.ident.fst A B => fst + | Compilers.ident.snd A B => snd + | Compilers.ident.pair_rect A B T => pair_rect + | Compilers.ident.bool_rect T => bool_rect + | Compilers.ident.nat_rect P => nat_rect + | Compilers.ident.list_rect A P => list_rect + | Compilers.ident.list_case A P => list_case + | Compilers.ident.List_length T => List_length + | Compilers.ident.List_seq => List_seq + | Compilers.ident.List_repeat A => List_repeat + | Compilers.ident.List_combine A B => List_combine + | Compilers.ident.List_map A B => List_map + | Compilers.ident.List_app A => List_app + | Compilers.ident.List_rev A => List_rev + | Compilers.ident.List_flat_map A B => List_flat_map + | Compilers.ident.List_partition A => List_partition + | Compilers.ident.List_fold_right A B => List_fold_right + | Compilers.ident.List_update_nth T => List_update_nth + | Compilers.ident.List_nth_default T => List_nth_default + | 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_eqb => Z_eqb + | Compilers.ident.Z_leb => Z_leb + | Compilers.ident.Z_of_nat => Z_of_nat + | Compilers.ident.Z_shiftr offset => Z_shiftr + | Compilers.ident.Z_shiftl offset => Z_shiftl + | Compilers.ident.Z_land mask => Z_land + | Compilers.ident.Z_mul_split => Z_mul_split + | Compilers.ident.Z_mul_split_concrete s => Z_mul_split_concrete + | Compilers.ident.Z_add_get_carry => Z_add_get_carry + | Compilers.ident.Z_add_get_carry_concrete s => Z_add_get_carry_concrete + | 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_add_with_get_carry_concrete s => Z_add_with_get_carry_concrete + | Compilers.ident.Z_sub_get_borrow => Z_sub_get_borrow + | Compilers.ident.Z_sub_get_borrow_concrete s => Z_sub_get_borrow_concrete + | Compilers.ident.Z_sub_with_get_borrow => Z_sub_with_get_borrow + | Compilers.ident.Z_sub_with_get_borrow_concrete s => Z_sub_with_get_borrow_concrete + | Compilers.ident.Z_zselect => Z_zselect + | Compilers.ident.Z_add_modulo => Z_add_modulo + | Compilers.ident.Z_rshi => Z_rshi + | Compilers.ident.Z_rshi_concrete s offset => Z_rshi_concrete + | Compilers.ident.Z_cc_m => Z_cc_m + | Compilers.ident.Z_cc_m_concrete s => Z_cc_m_concrete + | Compilers.ident.Z_neg_snd => Z_neg_snd + | Compilers.ident.Z_cast range => Z_cast + | Compilers.ident.Z_cast2 range => Z_cast2 + | 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 + end. + + Definition arg_types (idc : ident) : option Type + := match idc return option Type with + | LiteralUnit => @Some Type (base.interp Compilers.base.type.unit) + | LiteralZ => @Some Type (base.interp Compilers.base.type.Z) + | LiteralBool => @Some Type (base.interp Compilers.base.type.bool) + | LiteralNat => @Some Type (base.interp Compilers.base.type.nat) + | Nat_succ => None + | Nat_pred => None + | Nat_max => None + | Nat_mul => None + | Nat_add => None + | Nat_sub => None + | nil => None + | cons => None + | pair => None + | fst => None + | snd => None + | pair_rect => None + | bool_rect => None + | nat_rect => None + | list_rect => None + | list_case => None + | List_length => None + | List_seq => None + | List_repeat => None + | List_combine => None + | List_map => None + | List_app => None + | List_rev => None + | List_flat_map => None + | List_partition => None + | List_fold_right => None + | List_update_nth => None + | List_nth_default => None + | Z_add => None + | Z_mul => None + | Z_pow => None + | Z_sub => None + | Z_opp => None + | Z_div => None + | Z_modulo => None + | Z_eqb => None + | Z_leb => None + | Z_of_nat => None + | Z_shiftr => @Some Type Z + | Z_shiftl => @Some Type Z + | Z_land => @Some Type Z + | Z_mul_split => None + | Z_mul_split_concrete => @Some Type Z + | Z_add_get_carry => None + | Z_add_get_carry_concrete => @Some Type Z + | Z_add_with_carry => None + | Z_add_with_get_carry => None + | Z_add_with_get_carry_concrete => @Some Type Z + | Z_sub_get_borrow => None + | Z_sub_get_borrow_concrete => @Some Type Z + | Z_sub_with_get_borrow => None + | Z_sub_with_get_borrow_concrete => @Some Type Z + | Z_zselect => None + | Z_add_modulo => None + | Z_rshi => None + | Z_rshi_concrete => @Some Type (Z * Z) + | Z_cc_m => None + | Z_cc_m_concrete => @Some Type Z + | Z_neg_snd => None + | Z_cast => @Some Type zrange + | Z_cast2 => @Some Type (zrange * zrange) + | fancy_add => @Some Type (Z * Z) + | fancy_addc => @Some Type (Z * Z) + | fancy_sub => @Some Type (Z * Z) + | fancy_subb => @Some Type (Z * Z) + | fancy_mulll => @Some Type Z + | fancy_mullh => @Some Type Z + | fancy_mulhl => @Some Type Z + | fancy_mulhh => @Some Type Z + | fancy_rshi => @Some Type (Z * Z) + | fancy_selc => None + | fancy_selm => @Some Type Z + | fancy_sell => None + | fancy_addm => None + end%type. + + Definition full_types (idc : ident) : Type + := match idc return Type with + | LiteralUnit => base.interp Compilers.base.type.unit + | LiteralZ => base.interp Compilers.base.type.Z + | LiteralBool => base.interp Compilers.base.type.bool + | LiteralNat => base.interp Compilers.base.type.nat + | Nat_succ => unit + | Nat_pred => unit + | Nat_max => unit + | Nat_mul => unit + | Nat_add => unit + | Nat_sub => unit + | nil => Compilers.base.type.type + | cons => Compilers.base.type.type + | pair => Compilers.base.type.type * Compilers.base.type.type + | fst => Compilers.base.type.type * Compilers.base.type.type + | snd => Compilers.base.type.type * Compilers.base.type.type + | pair_rect => Compilers.base.type.type * Compilers.base.type.type * Compilers.base.type.type + | bool_rect => Compilers.base.type.type + | nat_rect => Compilers.base.type.type + | list_rect => Compilers.base.type.type * Compilers.base.type.type + | list_case => Compilers.base.type.type * Compilers.base.type.type + | List_length => Compilers.base.type.type + | List_seq => unit + | List_repeat => Compilers.base.type.type + | List_combine => Compilers.base.type.type * Compilers.base.type.type + | List_map => Compilers.base.type.type * Compilers.base.type.type + | List_app => Compilers.base.type.type + | List_rev => Compilers.base.type.type + | List_flat_map => Compilers.base.type.type * Compilers.base.type.type + | List_partition => Compilers.base.type.type + | List_fold_right => Compilers.base.type.type * Compilers.base.type.type + | List_update_nth => Compilers.base.type.type + | List_nth_default => Compilers.base.type.type + | Z_add => unit + | Z_mul => unit + | Z_pow => unit + | Z_sub => unit + | Z_opp => unit + | Z_div => unit + | Z_modulo => unit + | Z_eqb => unit + | Z_leb => unit + | Z_of_nat => unit + | Z_shiftr => Z + | Z_shiftl => Z + | Z_land => Z + | Z_mul_split => unit + | Z_mul_split_concrete => Z + | Z_add_get_carry => unit + | Z_add_get_carry_concrete => Z + | Z_add_with_carry => unit + | Z_add_with_get_carry => unit + | Z_add_with_get_carry_concrete => Z + | Z_sub_get_borrow => unit + | Z_sub_get_borrow_concrete => Z + | Z_sub_with_get_borrow => unit + | Z_sub_with_get_borrow_concrete => Z + | Z_zselect => unit + | Z_add_modulo => unit + | Z_rshi => unit + | Z_rshi_concrete => Z * Z + | Z_cc_m => unit + | Z_cc_m_concrete => Z + | Z_neg_snd => unit + | Z_cast => zrange + | Z_cast2 => zrange * zrange + | 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 bind_args {t} (idc : Compilers.ident.ident t) : match arg_types (of_typed_ident idc) return Type with Some t => t | None => unit end + := match idc return match arg_types (of_typed_ident idc) return Type with Some t => t | None => unit end with + | Compilers.ident.LiteralUnit v => v + | Compilers.ident.LiteralZ v => v + | Compilers.ident.LiteralBool v => v + | Compilers.ident.LiteralNat v => v + | 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.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.pair_rect A B T => tt + | Compilers.ident.bool_rect T => tt + | Compilers.ident.nat_rect P => tt + | Compilers.ident.list_rect A P => tt + | Compilers.ident.list_case A P => tt + | Compilers.ident.List_length T => tt + | Compilers.ident.List_seq => 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.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_eqb => tt + | Compilers.ident.Z_leb => tt + | Compilers.ident.Z_of_nat => tt + | Compilers.ident.Z_shiftr offset => offset + | Compilers.ident.Z_shiftl offset => offset + | Compilers.ident.Z_land mask => mask + | Compilers.ident.Z_mul_split => tt + | Compilers.ident.Z_mul_split_concrete s => s + | Compilers.ident.Z_add_get_carry => tt + | Compilers.ident.Z_add_get_carry_concrete s => s + | Compilers.ident.Z_add_with_carry => tt + | Compilers.ident.Z_add_with_get_carry => tt + | Compilers.ident.Z_add_with_get_carry_concrete s => s + | Compilers.ident.Z_sub_get_borrow => tt + | Compilers.ident.Z_sub_get_borrow_concrete s => s + | Compilers.ident.Z_sub_with_get_borrow => tt + | Compilers.ident.Z_sub_with_get_borrow_concrete s => s + | Compilers.ident.Z_zselect => tt + | Compilers.ident.Z_add_modulo => tt + | Compilers.ident.Z_rshi => tt + | Compilers.ident.Z_rshi_concrete s offset => (s, offset) + | Compilers.ident.Z_cc_m => tt + | Compilers.ident.Z_cc_m_concrete s => s + | Compilers.ident.Z_neg_snd => tt + | Compilers.ident.Z_cast range => range + | Compilers.ident.Z_cast2 range => range + | Compilers.ident.fancy_add log2wordmax imm => (log2wordmax, imm) + | Compilers.ident.fancy_addc log2wordmax imm => (log2wordmax, imm) + | Compilers.ident.fancy_sub log2wordmax imm => (log2wordmax, imm) + | Compilers.ident.fancy_subb log2wordmax imm => (log2wordmax, imm) + | Compilers.ident.fancy_mulll log2wordmax => log2wordmax + | Compilers.ident.fancy_mullh log2wordmax => log2wordmax + | Compilers.ident.fancy_mulhl log2wordmax => log2wordmax + | Compilers.ident.fancy_mulhh log2wordmax => log2wordmax + | Compilers.ident.fancy_rshi log2wordmax x => (log2wordmax, x) + | Compilers.ident.fancy_selc => tt + | Compilers.ident.fancy_selm log2wordmax => log2wordmax + | Compilers.ident.fancy_sell => tt + | Compilers.ident.fancy_addm => tt + end%cps. + + Definition invert_bind_args {t} (idc : Compilers.ident.ident t) (pidc : ident) : option (full_types pidc) + := match pidc, idc return option (full_types pidc) with + | LiteralUnit, Compilers.ident.LiteralUnit v => Some v + | LiteralZ, Compilers.ident.LiteralZ v => Some v + | LiteralBool, Compilers.ident.LiteralBool v => Some v + | LiteralNat, Compilers.ident.LiteralNat v => Some v + | Nat_succ, Compilers.ident.Nat_succ => Some tt + | Nat_pred, Compilers.ident.Nat_pred => Some tt + | Nat_max, Compilers.ident.Nat_max => Some tt + | Nat_mul, Compilers.ident.Nat_mul => Some tt + | Nat_add, Compilers.ident.Nat_add => Some tt + | Nat_sub, Compilers.ident.Nat_sub => Some tt + | nil, Compilers.ident.nil t => Some t + | cons, Compilers.ident.cons t => Some t + | pair, Compilers.ident.pair A B => Some (A, B) + | fst, Compilers.ident.fst A B => Some (A, B) + | snd, Compilers.ident.snd A B => Some (A, B) + | pair_rect, Compilers.ident.pair_rect A B T => Some (A, B, T) + | bool_rect, Compilers.ident.bool_rect T => Some T + | nat_rect, Compilers.ident.nat_rect P => Some P + | list_rect, Compilers.ident.list_rect A P => Some (A, P) + | list_case, Compilers.ident.list_case A P => Some (A, P) + | List_length, Compilers.ident.List_length T => Some T + | List_seq, Compilers.ident.List_seq => Some tt + | List_repeat, Compilers.ident.List_repeat A => Some A + | List_combine, Compilers.ident.List_combine A B => Some (A, B) + | List_map, Compilers.ident.List_map A B => Some (A, B) + | List_app, Compilers.ident.List_app A => Some A + | List_rev, Compilers.ident.List_rev A => Some A + | List_flat_map, Compilers.ident.List_flat_map A B => Some (A, B) + | List_partition, Compilers.ident.List_partition A => Some A + | List_fold_right, Compilers.ident.List_fold_right A B => Some (A, B) + | List_update_nth, Compilers.ident.List_update_nth T => Some T + | List_nth_default, Compilers.ident.List_nth_default T => Some T + | Z_add, Compilers.ident.Z_add => Some tt + | Z_mul, Compilers.ident.Z_mul => Some tt + | Z_pow, Compilers.ident.Z_pow => Some tt + | Z_sub, Compilers.ident.Z_sub => Some tt + | Z_opp, Compilers.ident.Z_opp => Some tt + | Z_div, Compilers.ident.Z_div => Some tt + | Z_modulo, Compilers.ident.Z_modulo => Some tt + | Z_eqb, Compilers.ident.Z_eqb => Some tt + | Z_leb, Compilers.ident.Z_leb => Some tt + | Z_of_nat, Compilers.ident.Z_of_nat => Some tt + | Z_shiftr, Compilers.ident.Z_shiftr offset => Some offset + | Z_shiftl, Compilers.ident.Z_shiftl offset => Some offset + | Z_land, Compilers.ident.Z_land mask => Some mask + | Z_mul_split, Compilers.ident.Z_mul_split => Some tt + | Z_mul_split_concrete, Compilers.ident.Z_mul_split_concrete s => Some s + | Z_add_get_carry, Compilers.ident.Z_add_get_carry => Some tt + | Z_add_get_carry_concrete, Compilers.ident.Z_add_get_carry_concrete s => Some s + | Z_add_with_carry, Compilers.ident.Z_add_with_carry => Some tt + | Z_add_with_get_carry, Compilers.ident.Z_add_with_get_carry => Some tt + | Z_add_with_get_carry_concrete, Compilers.ident.Z_add_with_get_carry_concrete s => Some s + | Z_sub_get_borrow, Compilers.ident.Z_sub_get_borrow => Some tt + | Z_sub_get_borrow_concrete, Compilers.ident.Z_sub_get_borrow_concrete s => Some s + | Z_sub_with_get_borrow, Compilers.ident.Z_sub_with_get_borrow => Some tt + | Z_sub_with_get_borrow_concrete, Compilers.ident.Z_sub_with_get_borrow_concrete s => Some s + | Z_zselect, Compilers.ident.Z_zselect => Some tt + | Z_add_modulo, Compilers.ident.Z_add_modulo => Some tt + | Z_rshi, Compilers.ident.Z_rshi => Some tt + | Z_rshi_concrete, Compilers.ident.Z_rshi_concrete s offset => Some (s, offset) + | Z_cc_m, Compilers.ident.Z_cc_m => Some tt + | Z_cc_m_concrete, Compilers.ident.Z_cc_m_concrete s => Some s + | Z_neg_snd, Compilers.ident.Z_neg_snd => Some tt + | Z_cast, Compilers.ident.Z_cast range => Some range + | Z_cast2, Compilers.ident.Z_cast2 range => Some range + | fancy_add, Compilers.ident.fancy_add log2wordmax imm => Some (log2wordmax, imm) + | fancy_addc, Compilers.ident.fancy_addc log2wordmax imm => Some (log2wordmax, imm) + | fancy_sub, Compilers.ident.fancy_sub log2wordmax imm => Some (log2wordmax, imm) + | fancy_subb, Compilers.ident.fancy_subb log2wordmax imm => Some (log2wordmax, imm) + | fancy_mulll, Compilers.ident.fancy_mulll log2wordmax => Some log2wordmax + | fancy_mullh, Compilers.ident.fancy_mullh log2wordmax => Some log2wordmax + | fancy_mulhl, Compilers.ident.fancy_mulhl log2wordmax => Some log2wordmax + | fancy_mulhh, Compilers.ident.fancy_mulhh log2wordmax => Some log2wordmax + | fancy_rshi, Compilers.ident.fancy_rshi log2wordmax x => Some (log2wordmax, x) + | fancy_selc, Compilers.ident.fancy_selc => Some tt + | fancy_selm, Compilers.ident.fancy_selm log2wordmax => Some log2wordmax + | fancy_sell, Compilers.ident.fancy_sell => Some tt + | fancy_addm, Compilers.ident.fancy_addm => Some tt + | LiteralUnit, _ + | LiteralZ, _ + | LiteralBool, _ + | LiteralNat, _ + | Nat_succ, _ + | Nat_pred, _ + | Nat_max, _ + | Nat_mul, _ + | Nat_add, _ + | Nat_sub, _ + | nil, _ + | cons, _ + | pair, _ + | fst, _ + | snd, _ + | pair_rect, _ + | bool_rect, _ + | nat_rect, _ + | list_rect, _ + | list_case, _ + | List_length, _ + | List_seq, _ + | List_repeat, _ + | List_combine, _ + | List_map, _ + | List_app, _ + | List_rev, _ + | List_flat_map, _ + | List_partition, _ + | List_fold_right, _ + | List_update_nth, _ + | List_nth_default, _ + | Z_add, _ + | Z_mul, _ + | Z_pow, _ + | Z_sub, _ + | Z_opp, _ + | Z_div, _ + | Z_modulo, _ + | Z_eqb, _ + | Z_leb, _ + | Z_of_nat, _ + | Z_shiftr, _ + | Z_shiftl, _ + | Z_land, _ + | Z_mul_split, _ + | Z_mul_split_concrete, _ + | Z_add_get_carry, _ + | Z_add_get_carry_concrete, _ + | Z_add_with_carry, _ + | Z_add_with_get_carry, _ + | Z_add_with_get_carry_concrete, _ + | Z_sub_get_borrow, _ + | Z_sub_get_borrow_concrete, _ + | Z_sub_with_get_borrow, _ + | Z_sub_with_get_borrow_concrete, _ + | Z_zselect, _ + | Z_add_modulo, _ + | Z_rshi, _ + | Z_rshi_concrete, _ + | Z_cc_m, _ + | Z_cc_m_concrete, _ + | Z_neg_snd, _ + | Z_cast, _ + | Z_cast2, _ + | 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, _ + => None + end%cps. + + Local Notation eta2 x := (Datatypes.fst x, Datatypes.snd x) (only parsing). + Local Notation eta3 x := (eta2 (Datatypes.fst x), Datatypes.snd x) (only parsing). + + Definition type_of (pidc : ident) : full_types pidc -> Compilers.type Compilers.base.type + := match pidc return full_types pidc -> _ with + | LiteralUnit => fun v => (type.base (Compilers.base.type.type_base Compilers.base.type.unit)) + | LiteralZ => fun v => (type.base (Compilers.base.type.type_base Compilers.base.type.Z)) + | LiteralBool => fun v => (type.base (Compilers.base.type.type_base Compilers.base.type.bool)) + | LiteralNat => fun v => (type.base (Compilers.base.type.type_base Compilers.base.type.nat)) + | Nat_succ => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%etype + | Nat_pred => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.nat))%etype + | 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))%etype + | 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))%etype + | 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))%etype + | 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))%etype + | 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))%etype + | pair => fun arg => let '(A, B) := eta2 arg in (type.base A -> type.base B -> type.base (A * B)%etype)%etype + | fst => fun arg => let '(A, B) := eta2 arg in (type.base (A * B)%etype -> type.base A)%etype + | snd => fun arg => let '(A, B) := eta2 arg in (type.base (A * B)%etype -> type.base B)%etype + | pair_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)%etype + | 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)%etype + | 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)%etype + | 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)%etype + | 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)%etype + | List_length => fun T => (type.base (Compilers.base.type.list T) -> type.base (Compilers.base.type.type_base base.type.nat))%etype + | 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)))%etype + | List_repeat => fun A => (type.base A -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.list A))%etype + | 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)))%etype + | 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))%etype + | 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))%etype + | List_rev => fun A => (type.base (Compilers.base.type.list A) -> type.base (Compilers.base.type.list A))%etype + | 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))%etype + | 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)%etype + | 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)%etype + | 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))%etype + | 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)%etype + | 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))%etype + | 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))%etype + | 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))%etype + | 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))%etype + | Z_opp => fun _ => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%etype + | 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))%etype + | 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))%etype + | 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))%etype + | 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))%etype + | Z_of_nat => fun _ => (type.base (Compilers.base.type.type_base base.type.nat) -> type.base (Compilers.base.type.type_base base.type.Z))%etype + | Z_shiftr => fun offset => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%etype + | Z_shiftl => fun offset => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%etype + | Z_land => fun mask => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%etype + | 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)%etype + | Z_mul_split_concrete => fun s => (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)%etype + | 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)%etype + | Z_add_get_carry_concrete => fun s => (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)%etype + | 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))%etype + | 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)%etype + | Z_add_with_get_carry_concrete => fun s => (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)%etype + | 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)%etype + | Z_sub_get_borrow_concrete => fun s => (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)%etype + | 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)%etype + | Z_sub_with_get_borrow_concrete => fun s => (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)%etype + | 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))%etype + | 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))%etype + | 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))%etype + | Z_rshi_concrete => fun arg => let '(s, offset) := eta2 arg in (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))%etype + | 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))%etype + | Z_cc_m_concrete => fun s => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%etype + | Z_neg_snd => fun _ => (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)%etype + | Z_cast => fun range => (type.base (Compilers.base.type.type_base base.type.Z) -> type.base (Compilers.base.type.type_base base.type.Z))%etype + | 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)%etype + | 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)%etype + | 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)%etype + | 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)%etype + | 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)%etype + | 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))%etype + | 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))%etype + | 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))%etype + | 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))%etype + | 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))%etype + | 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))%etype + | 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))%etype + | 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))%etype + | 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))%etype + end. + + 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 + | LiteralUnit => fun v => @Compilers.ident.LiteralUnit v + | LiteralZ => fun v => @Compilers.ident.LiteralZ v + | LiteralBool => fun v => @Compilers.ident.LiteralBool v + | LiteralNat => fun v => @Compilers.ident.LiteralNat 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 + | nil => fun t => @Compilers.ident.nil t + | cons => fun t => @Compilers.ident.cons t + | pair => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of pair args') with (A, B) => @Compilers.ident.pair A B end + | fst => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of fst args') with (A, B) => @Compilers.ident.fst A B end + | snd => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of snd args') with (A, B) => @Compilers.ident.snd A B end + | pair_rect => fun arg => match eta3 arg as args' return Compilers.ident.ident (type_of pair_rect args') with (A, B, T) => @Compilers.ident.pair_rect A B T end + | bool_rect => fun T => @Compilers.ident.bool_rect T + | nat_rect => fun P => @Compilers.ident.nat_rect P + | list_rect => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of list_rect args') with (A, P) => @Compilers.ident.list_rect A P end + | list_case => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of list_case args') with (A, P) => @Compilers.ident.list_case A P end + | List_length => fun T => @Compilers.ident.List_length T + | List_seq => fun _ => @Compilers.ident.List_seq + | List_repeat => fun A => @Compilers.ident.List_repeat A + | List_combine => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of List_combine args') with (A, B) => @Compilers.ident.List_combine A B end + | List_map => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of List_map args') with (A, B) => @Compilers.ident.List_map A B end + | 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 args' return Compilers.ident.ident (type_of List_flat_map args') 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 args' return Compilers.ident.ident (type_of List_fold_right args') 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 + | 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_eqb => fun _ => @Compilers.ident.Z_eqb + | Z_leb => fun _ => @Compilers.ident.Z_leb + | Z_of_nat => fun _ => @Compilers.ident.Z_of_nat + | Z_shiftr => fun offset => @Compilers.ident.Z_shiftr offset + | Z_shiftl => fun offset => @Compilers.ident.Z_shiftl offset + | Z_land => fun mask => @Compilers.ident.Z_land mask + | Z_mul_split => fun _ => @Compilers.ident.Z_mul_split + | Z_mul_split_concrete => fun s => @Compilers.ident.Z_mul_split_concrete s + | Z_add_get_carry => fun _ => @Compilers.ident.Z_add_get_carry + | Z_add_get_carry_concrete => fun s => @Compilers.ident.Z_add_get_carry_concrete s + | 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_add_with_get_carry_concrete => fun s => @Compilers.ident.Z_add_with_get_carry_concrete s + | Z_sub_get_borrow => fun _ => @Compilers.ident.Z_sub_get_borrow + | Z_sub_get_borrow_concrete => fun s => @Compilers.ident.Z_sub_get_borrow_concrete s + | Z_sub_with_get_borrow => fun _ => @Compilers.ident.Z_sub_with_get_borrow + | Z_sub_with_get_borrow_concrete => fun s => @Compilers.ident.Z_sub_with_get_borrow_concrete s + | Z_zselect => fun _ => @Compilers.ident.Z_zselect + | Z_add_modulo => fun _ => @Compilers.ident.Z_add_modulo + | Z_rshi => fun _ => @Compilers.ident.Z_rshi + | Z_rshi_concrete => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of Z_rshi_concrete args') with (s, offset) => @Compilers.ident.Z_rshi_concrete s offset end + | Z_cc_m => fun _ => @Compilers.ident.Z_cc_m + | Z_cc_m_concrete => fun s => @Compilers.ident.Z_cc_m_concrete s + | Z_neg_snd => fun _ => @Compilers.ident.Z_neg_snd + | Z_cast => fun range => @Compilers.ident.Z_cast range + | Z_cast2 => fun range => @Compilers.ident.Z_cast2 range + | fancy_add => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of fancy_add args') with (log2wordmax, imm) => @Compilers.ident.fancy_add log2wordmax imm end + | fancy_addc => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of fancy_addc args') with (log2wordmax, imm) => @Compilers.ident.fancy_addc log2wordmax imm end + | fancy_sub => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of fancy_sub args') with (log2wordmax, imm) => @Compilers.ident.fancy_sub log2wordmax imm end + | fancy_subb => fun arg => match eta2 arg as args' return Compilers.ident.ident (type_of fancy_subb args') 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 args' return Compilers.ident.ident (type_of fancy_rshi args') 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 + end. + + Definition retype_ident {t} (idc : Compilers.ident.ident t) : match arg_types (of_typed_ident idc) return Type with Some t => t | None => unit end -> Compilers.ident.ident t + := match idc in Compilers.ident.ident t return match arg_types (of_typed_ident idc) return Type with Some t => t | None => unit end -> Compilers.ident.ident t with + | Compilers.ident.LiteralUnit v => (fun v => @Compilers.ident.LiteralUnit v) : match arg_types (of_typed_ident (@Compilers.ident.LiteralUnit v)) return Type with Some t => t | None => unit end -> _ (* COQBUG(https://github.com/coq/coq/issues/7726) *) + | Compilers.ident.LiteralZ v => (fun v => @Compilers.ident.LiteralZ v) : match arg_types (of_typed_ident (@Compilers.ident.LiteralZ v)) return Type with Some t => t | None => unit end -> _ (* COQBUG(https://github.com/coq/coq/issues/7726) *) + | Compilers.ident.LiteralBool v => (fun v => @Compilers.ident.LiteralBool v) : match arg_types (of_typed_ident (@Compilers.ident.LiteralBool v)) return Type with Some t => t | None => unit end -> _ (* COQBUG(https://github.com/coq/coq/issues/7726) *) + | Compilers.ident.LiteralNat v => (fun v => @Compilers.ident.LiteralNat v) : match arg_types (of_typed_ident (@Compilers.ident.LiteralNat v)) return Type with Some t => t | None => unit end -> _ (* COQBUG(https://github.com/coq/coq/issues/7726) *) + | Compilers.ident.Nat_succ => fun _ => @Compilers.ident.Nat_succ + | Compilers.ident.Nat_pred => fun _ => @Compilers.ident.Nat_pred + | Compilers.ident.Nat_max => fun _ => @Compilers.ident.Nat_max + | Compilers.ident.Nat_mul => fun _ => @Compilers.ident.Nat_mul + | Compilers.ident.Nat_add => fun _ => @Compilers.ident.Nat_add + | Compilers.ident.Nat_sub => fun _ => @Compilers.ident.Nat_sub + | Compilers.ident.nil t => fun _ => @Compilers.ident.nil t + | Compilers.ident.cons t => fun _ => @Compilers.ident.cons t + | Compilers.ident.pair A B => fun _ => @Compilers.ident.pair A B + | Compilers.ident.fst A B => fun _ => @Compilers.ident.fst A B + | Compilers.ident.snd A B => fun _ => @Compilers.ident.snd A B + | Compilers.ident.pair_rect A B T => fun _ => @Compilers.ident.pair_rect A B T + | Compilers.ident.bool_rect T => fun _ => @Compilers.ident.bool_rect T + | Compilers.ident.nat_rect P => fun _ => @Compilers.ident.nat_rect P + | Compilers.ident.list_rect A P => fun _ => @Compilers.ident.list_rect A P + | Compilers.ident.list_case A P => fun _ => @Compilers.ident.list_case A P + | Compilers.ident.List_length T => fun _ => @Compilers.ident.List_length T + | Compilers.ident.List_seq => fun _ => @Compilers.ident.List_seq + | Compilers.ident.List_repeat A => fun _ => @Compilers.ident.List_repeat A + | Compilers.ident.List_combine A B => fun _ => @Compilers.ident.List_combine A B + | Compilers.ident.List_map A B => fun _ => @Compilers.ident.List_map A B + | Compilers.ident.List_app A => fun _ => @Compilers.ident.List_app A + | Compilers.ident.List_rev A => fun _ => @Compilers.ident.List_rev A + | Compilers.ident.List_flat_map A B => fun _ => @Compilers.ident.List_flat_map A B + | Compilers.ident.List_partition A => fun _ => @Compilers.ident.List_partition A + | Compilers.ident.List_fold_right A B => fun _ => @Compilers.ident.List_fold_right A B + | Compilers.ident.List_update_nth T => fun _ => @Compilers.ident.List_update_nth T + | Compilers.ident.List_nth_default T => fun _ => @Compilers.ident.List_nth_default T + | Compilers.ident.Z_add => fun _ => @Compilers.ident.Z_add + | Compilers.ident.Z_mul => fun _ => @Compilers.ident.Z_mul + | Compilers.ident.Z_pow => fun _ => @Compilers.ident.Z_pow + | Compilers.ident.Z_sub => fun _ => @Compilers.ident.Z_sub + | Compilers.ident.Z_opp => fun _ => @Compilers.ident.Z_opp + | Compilers.ident.Z_div => fun _ => @Compilers.ident.Z_div + | Compilers.ident.Z_modulo => fun _ => @Compilers.ident.Z_modulo + | Compilers.ident.Z_eqb => fun _ => @Compilers.ident.Z_eqb + | Compilers.ident.Z_leb => fun _ => @Compilers.ident.Z_leb + | Compilers.ident.Z_of_nat => fun _ => @Compilers.ident.Z_of_nat + | Compilers.ident.Z_shiftr offset => fun offset => @Compilers.ident.Z_shiftr offset + | Compilers.ident.Z_shiftl offset => fun offset => @Compilers.ident.Z_shiftl offset + | Compilers.ident.Z_land mask => fun mask => @Compilers.ident.Z_land mask + | Compilers.ident.Z_mul_split => fun _ => @Compilers.ident.Z_mul_split + | Compilers.ident.Z_mul_split_concrete s => fun s => @Compilers.ident.Z_mul_split_concrete s + | Compilers.ident.Z_add_get_carry => fun _ => @Compilers.ident.Z_add_get_carry + | Compilers.ident.Z_add_get_carry_concrete s => fun s => @Compilers.ident.Z_add_get_carry_concrete s + | Compilers.ident.Z_add_with_carry => fun _ => @Compilers.ident.Z_add_with_carry + | Compilers.ident.Z_add_with_get_carry => fun _ => @Compilers.ident.Z_add_with_get_carry + | Compilers.ident.Z_add_with_get_carry_concrete s => fun s => @Compilers.ident.Z_add_with_get_carry_concrete s + | Compilers.ident.Z_sub_get_borrow => fun _ => @Compilers.ident.Z_sub_get_borrow + | Compilers.ident.Z_sub_get_borrow_concrete s => fun s => @Compilers.ident.Z_sub_get_borrow_concrete s + | Compilers.ident.Z_sub_with_get_borrow => fun _ => @Compilers.ident.Z_sub_with_get_borrow + | Compilers.ident.Z_sub_with_get_borrow_concrete s => fun s => @Compilers.ident.Z_sub_with_get_borrow_concrete s + | Compilers.ident.Z_zselect => fun _ => @Compilers.ident.Z_zselect + | Compilers.ident.Z_add_modulo => fun _ => @Compilers.ident.Z_add_modulo + | Compilers.ident.Z_rshi => fun _ => @Compilers.ident.Z_rshi + | Compilers.ident.Z_rshi_concrete s offset => fun arg => let '(s, offset) := eta2 arg in @Compilers.ident.Z_rshi_concrete s offset + | Compilers.ident.Z_cc_m => fun _ => @Compilers.ident.Z_cc_m + | Compilers.ident.Z_cc_m_concrete s => fun s => @Compilers.ident.Z_cc_m_concrete s + | Compilers.ident.Z_neg_snd => fun _ => @Compilers.ident.Z_neg_snd + | Compilers.ident.Z_cast range => fun range => @Compilers.ident.Z_cast range + | Compilers.ident.Z_cast2 range => fun range => @Compilers.ident.Z_cast2 range + | Compilers.ident.fancy_add log2wordmax imm => fun arg => let '(log2wordmax, imm) := eta2 arg in @Compilers.ident.fancy_add log2wordmax imm + | Compilers.ident.fancy_addc log2wordmax imm => fun arg => let '(log2wordmax, imm) := eta2 arg in @Compilers.ident.fancy_addc log2wordmax imm + | Compilers.ident.fancy_sub log2wordmax imm => fun arg => let '(log2wordmax, imm) := eta2 arg in @Compilers.ident.fancy_sub log2wordmax imm + | Compilers.ident.fancy_subb log2wordmax imm => fun arg => let '(log2wordmax, imm) := eta2 arg in @Compilers.ident.fancy_subb log2wordmax imm + | Compilers.ident.fancy_mulll log2wordmax => fun log2wordmax => @Compilers.ident.fancy_mulll log2wordmax + | Compilers.ident.fancy_mullh log2wordmax => fun log2wordmax => @Compilers.ident.fancy_mullh log2wordmax + | Compilers.ident.fancy_mulhl log2wordmax => fun log2wordmax => @Compilers.ident.fancy_mulhl log2wordmax + | Compilers.ident.fancy_mulhh log2wordmax => fun log2wordmax => @Compilers.ident.fancy_mulhh log2wordmax + | Compilers.ident.fancy_rshi log2wordmax x => fun arg => let '(log2wordmax, x) := eta2 arg in @Compilers.ident.fancy_rshi log2wordmax x + | Compilers.ident.fancy_selc => fun _ => @Compilers.ident.fancy_selc + | Compilers.ident.fancy_selm log2wordmax => fun log2wordmax => @Compilers.ident.fancy_selm log2wordmax + | Compilers.ident.fancy_sell => fun _ => @Compilers.ident.fancy_sell + | Compilers.ident.fancy_addm => fun _ => @Compilers.ident.fancy_addm + end. + + + (*===*) + End ident. + End pattern. +End Compilers. |